Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply unknownprop_10cfff1173259328ed05ac7e63c6e194463722e1152adf6ca3f775a31e4297bc with
λ x3 x4 : ι → ι → ι → ο . x4 x0 x1 x2 ⟶ ∀ x5 : ο . (∀ x6 x7 . equip (setsum x0 x6) x1 ⟶ equip (setprod x7 x6) x2 ⟶ x5) ⟶ (∀ x6 x7 . equip (setsum x1 x6) x0 ⟶ equip (setprod x7 x6) x2 ⟶ x5) ⟶ x5.
Let x3 of type ο be given.
Apply H0 with
x3.
Let x4 of type ι be given.
Apply H3 with
x3.
Let x5 of type ι be given.
Apply unknownprop_eb8e8f72a91f1b934993d4cb19c84c8270f73a3626f3022b683d960a7fef89cb with
and (equip (setsum x0 x4) x1) (equip (setprod x5 x4) x2),
and (equip (setsum x1 x4) x0) (equip (setprod x5 x4) x2),
x3 leaving 3 subgoals.
The subproof is completed by applying H4.
Apply andE with
equip (setsum x0 x4) x1,
equip (setprod x5 x4) x2,
x3 leaving 2 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H1 with x4, x5.
Apply andE with
equip (setsum x1 x4) x0,
equip (setprod x5 x4) x2,
x3 leaving 2 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H2 with x4, x5.