Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Let x3 of type ι be given.

Let x4 of type ι be given.

Assume H0: equip (setsum x0 x3) x1.

Assume H1: equip (setprod x4 x3) x2.

Apply unknownprop_10cfff1173259328ed05ac7e63c6e194463722e1152adf6ca3f775a31e4297bc with λ x5 x6 : ι → ι → ι → ο . x6 x0 x1 x2.

Let x5 of type ο be given.

Assume H2: ∀ x6 . (∃ x7 . or (and (equip (setsum x0 x6) x1) (equip (setprod x7 x6) x2)) (and (equip (setsum x1 x6) x0) (equip (setprod x7 x6) x2))) ⟶ x5.

Apply H2 with x3.

Let x6 of type ο be given.

Assume H3: ∀ x7 . or (and (equip (setsum x0 x3) x1) (equip (setprod x7 x3) x2)) (and (equip (setsum x1 x3) x0) (equip (setprod x7 x3) x2)) ⟶ x6.

Apply H3 with x4.

Apply unknownprop_7c688f24c3595bc4b513e911d7f551c8ccfedc804a6c15c02d25d01a2996aec6 with and (equip (setsum x0 x3) x1) (equip (setprod x4 x3) x2), and (equip (setsum x1 x3) x0) (equip (setprod x4 x3) x2).

Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with equip (setsum x0 x3) x1, equip (setprod x4 x3) x2 leaving 2 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

■

Proofgold Proof