Let x0 of type ι be given.
Apply set_ext with
setsum 1 x0,
Inj1 x0 leaving 2 subgoals.
Let x1 of type ι be given.
Apply setsum_Inj_inv with
1,
x0,
x1,
x1 ∈ Inj1 x0 leaving 3 subgoals.
The subproof is completed by applying H0.
Assume H1:
∃ x2 . and (x2 ∈ 1) (x1 = Inj0 x2).
Apply exandE_i with
λ x2 . x2 ∈ 1,
λ x2 . x1 = Inj0 x2,
x1 ∈ Inj1 x0 leaving 2 subgoals.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Assume H2: x2 ∈ 1.
Apply H3 with
λ x3 x4 . x4 ∈ Inj1 x0.
Claim L4: x2 = 0
Apply SingE with
0,
x2.
Apply Subq_1_Sing0 with
x2.
The subproof is completed by applying H2.
Apply L4 with
λ x3 x4 . Inj0 x4 ∈ Inj1 x0.
Apply Inj0_0 with
λ x3 x4 . x4 ∈ Inj1 x0.
The subproof is completed by applying Inj1I1 with x0.
Assume H1:
∃ x2 . and (x2 ∈ x0) (x1 = Inj1 x2).
Apply exandE_i with
λ x2 . x2 ∈ x0,
λ x2 . x1 = Inj1 x2,
x1 ∈ Inj1 x0 leaving 2 subgoals.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Assume H2: x2 ∈ x0.
Apply H3 with
λ x3 x4 . x4 ∈ Inj1 x0.
Apply Inj1I2 with
x0,
x2.
The subproof is completed by applying H2.
Let x1 of type ι be given.
Apply Inj1E with
x0,
x1,
x1 ∈ setsum 1 x0 leaving 3 subgoals.
The subproof is completed by applying H0.
Assume H1: x1 = 0.
Apply H1 with
λ x2 x3 . x3 ∈ setsum 1 x0.
Apply Inj0_0 with
λ x2 x3 . x2 ∈ setsum 1 x0.
Apply Inj0_setsum with
1,
x0,
0.
The subproof is completed by applying In_0_1.
Assume H1:
∃ x2 . and (x2 ∈ x0) (x1 = Inj1 x2).
Apply exandE_i with
λ x2 . x2 ∈ x0,
λ x2 . x1 = Inj1 x2,
x1 ∈ setsum 1 x0 leaving 2 subgoals.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Assume H2: x2 ∈ x0.
Apply H3 with
λ x3 x4 . x4 ∈ setsum 1 x0.
Apply Inj1_setsum with
1,
x0,
x2.
The subproof is completed by applying H2.