Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Assume H0: nIn x2 2.

Apply Empty_eq with ap (setsum x0 x1) x2.

Let x3 of type ι be given.

Assume H1: x3 ∈ ap (setsum x0 x1) x2.

Claim L2: setsum x2 x3 ∈ setsum x0 x1

Apply apE with setsum x0 x1, x2, x3.

The subproof is completed by applying H1.

Apply pairE with x0, x1, setsum x2 x3, False leaving 3 subgoals.

The subproof is completed by applying L2.

Assume H3: ∃ x4 . and (x4 ∈ x0) (setsum x2 x3 = setsum 0 x4).

Apply exandE_i with λ x4 . x4 ∈ x0, λ x4 . setsum x2 x3 = setsum 0 x4, False leaving 2 subgoals.

The subproof is completed by applying H3.

Let x4 of type ι be given.

Assume H4: x4 ∈ x0.

Assume H5: setsum x2 x3 = setsum 0 x4.

Apply pair_inj with x2, x3, 0, x4, False leaving 2 subgoals.

The subproof is completed by applying H5.

Assume H6: x2 = 0.

Assume H7: x3 = x4.

Apply H0.

Apply H6 with λ x5 x6 . x6 ∈ 2.

The subproof is completed by applying In_0_2.

Assume H3: ∃ x4 . and (x4 ∈ x1) (setsum x2 x3 = setsum 1 x4).

Apply exandE_i with λ x4 . x4 ∈ x1, λ x4 . setsum x2 x3 = setsum 1 x4, False leaving 2 subgoals.

The subproof is completed by applying H3.

Let x4 of type ι be given.

Assume H4: x4 ∈ x1.

Assume H5: setsum x2 x3 = setsum 1 x4.

Apply pair_inj with x2, x3, 1, x4, False leaving 2 subgoals.

The subproof is completed by applying H5.

Assume H6: x2 = 1.

Assume H7: x3 = x4.

Apply H0.

Apply H6 with λ x5 x6 . x6 ∈ 2.

The subproof is completed by applying In_1_2.

■

Proofgold Proof