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.
Let x5 of type ι be given.
Let x6 of type ι be given.
Assume H3: x3 = x4 ⟶ ∀ x7 : ο . x7.
Assume H6: ∀ x7 . x7 ∈ x0 ⟶ x2 x7 ∈ x1.
Assume H7:
∀ x7 . x7 ∈ x1 ⟶ or (equip {x8 ∈ x0|x2 x8 = x7} x3) (equip {x8 ∈ x0|x2 x8 = x7} x4).
Assume H8:
equip {x7 ∈ x1|equip {x8 ∈ x0|x2 x8 = x7} x3} x5.
Assume H9:
equip {x7 ∈ x1|equip {x8 ∈ x0|x2 x8 = x7} x4} x6.
Apply unknownprop_8e052d85b2d476997756a4d2563048c027eabd3d70c30d840e8aa53708c6c883 with
add_nat (mul_nat x5 x3) (mul_nat x6 x4),
x0 leaving 3 subgoals.
Apply add_nat_p with
mul_nat x5 x3,
mul_nat x6 x4 leaving 2 subgoals.
Apply mul_nat_p with
x5,
x3 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H1.
Apply mul_nat_p with
x6,
x4 leaving 2 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H2.
The subproof is completed by applying H0.
Apply equip_tra with
add_nat (mul_nat x5 x3) (mul_nat x6 x4),
setsum (mul_nat x5 x3) (mul_nat x6 x4),
x0 leaving 2 subgoals.
Apply unknownprop_80fb4e499c5b9d344e7e79a37790e81cc16e6fd6cd87e88e961f3c8c4d6d418f with
mul_nat x5 x3,
mul_nat x6 x4,
mul_nat x5 x3,
mul_nat x6 x4 leaving 4 subgoals.
Apply mul_nat_p with
x5,
x3 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H1.
Apply mul_nat_p with
x6,
x4 leaving 2 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H2.
The subproof is completed by applying equip_ref with
mul_nat x5 x3.
The subproof is completed by applying equip_ref with
mul_nat x6 x4.
Apply L10 with
λ x7 x8 . equip (setsum (mul_nat x5 x3) (mul_nat x6 x4)) x7.
Apply equip_sym with
binunion (famunion {x7 ∈ x1|equip {x8 ∈ x0|x2 x8 = x7} x3} (λ x7 . {x8 ∈ x0|x2 x8 = x7})) (famunion {x7 ∈ x1|equip {x8 ∈ x0|x2 x8 = x7} x4} (λ x7 . {x8 ∈ x0|x2 x8 = x7})),
setsum (mul_nat x5 x3) (mul_nat x6 x4).
Apply unknownprop_8fed54475e70b18fbe9db03f1a81cd38ab9b210f0bea8d2bb706323c288b83da with
famunion {x7 ∈ x1|equip {x8 ∈ x0|x2 x8 = x7} x3} (λ x7 . {x8 ∈ x0|x2 x8 = x7}),
famunion {x7 ∈ x1|equip {x8 ∈ x0|x2 x8 = x7} x4} (λ x7 . {x8 ∈ x0|x2 x8 = x7}),
mul_nat x5 x3,
mul_nat x6 x4 leaving 3 subgoals.
Apply equip_tra with
famunion {x7 ∈ x1|equip {x8 ∈ x0|x2 x8 = x7} x3} (λ x7 . {x8 ∈ x0|x2 x8 = x7}),
setprod x5 x3,
mul_nat x5 x3 leaving 2 subgoals.
Apply unknownprop_c46d2ba0f36de9ca6b6266a654990ec059931cc2e555c517d90e20a2533a7a20 with
{x7 ∈ x1|equip {x8 ∈ x0|x2 x8 = x7} x3},
x5,
x3,
λ x7 . {x8 ∈ x0|x2 x8 = x7} leaving 3 subgoals.
The subproof is completed by applying H8.
Let x7 of type ι be given.
Assume H11:
x7 ∈ {x8 ∈ x1|equip {x9 ∈ x0|...} ...}.