Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Apply nat_ind with
λ x4 . ∀ x5 . equip x4 x5 ⟶ equip (mul_nat x0 x4) (setprod x2 x5) leaving 2 subgoals.
Let x4 of type ι be given.
Apply mul_nat_0R with
x0,
λ x5 x6 . equip x6 (setprod x2 x4).
Apply unknownprop_b1ab55fb3adc1f5608875c7150ec0901fc5d8b2cbdf1e5df6d670947db1f7326 with
x4,
λ x5 x6 . equip 0 (setprod x2 x6) leaving 2 subgoals.
The subproof is completed by applying H4.
Apply unknownprop_6e647c4b45e4fa58103006b82d03b760d3cc12e2b54a94fc09cdbc9261d55759 with
x2,
λ x5 x6 . equip 0 x6.
The subproof is completed by applying equip_ref with 0.
Let x4 of type ι be given.
Let x5 of type ι be given.
Apply mul_nat_SR with
x0,
x4,
λ x6 x7 . equip x7 (setprod x2 x5) leaving 2 subgoals.
The subproof is completed by applying H4.
Apply H6 with
equip (add_nat x0 (mul_nat x0 x4)) (setprod x2 x5).
Let x6 of type ι → ι be given.
Apply H7 with
equip (add_nat x0 (mul_nat x0 x4)) (setprod x2 x5).
Assume H8:
and (∀ x7 . x7 ∈ ordsucc x4 ⟶ x6 x7 ∈ x5) (∀ x7 . x7 ∈ ordsucc x4 ⟶ ∀ x8 . x8 ∈ ordsucc x4 ⟶ x6 x7 = x6 x8 ⟶ x7 = x8).
Apply H8 with
(∀ x7 . x7 ∈ x5 ⟶ ∃ x8 . and (x8 ∈ ordsucc x4) (x6 x8 = x7)) ⟶ equip (add_nat x0 (mul_nat x0 x4)) (setprod x2 x5).
Assume H9:
∀ x7 . x7 ∈ ordsucc x4 ⟶ x6 x7 ∈ x5.
Assume H10:
∀ x7 . x7 ∈ ordsucc x4 ⟶ ∀ x8 . x8 ∈ ordsucc x4 ⟶ x6 x7 = x6 x8 ⟶ x7 = x8.
Assume H11:
∀ x7 . x7 ∈ x5 ⟶ ∃ x8 . and (x8 ∈ ordsucc x4) (x6 x8 = x7).
Apply equip_tra with
add_nat x0 (mul_nat x0 x4),
setsum x2 (setprod x2 (setminus x5 (Sing (x6 x4)))),
setprod x2 x5 leaving 2 subgoals.
Apply unknownprop_80fb4e499c5b9d344e7e79a37790e81cc16e6fd6cd87e88e961f3c8c4d6d418f with
x0,
mul_nat x0 x4,
x2,
setprod x2 (setminus x5 (Sing (x6 x4))) leaving 4 subgoals.
The subproof is completed by applying H0.
Apply mul_nat_p with
x0,
x4 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H4.
The subproof is completed by applying H2.
Apply H5 with
setminus x5 (Sing (x6 x4)).
Let x7 of type ο be given.
Apply L4 with
x1,
x3 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H3.