Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Assume H0: setsum x1 x2 ∈ x0.

Apply proj1_pair_eq with x1, x2, λ x3 x4 . x3 ∈ {proj1 x5|x5 ∈ x0,∃ x6 . x5 = setsum x1 x6}.

Apply ReplSepI with x0, λ x3 . ∃ x4 . x3 = setsum x1 x4, proj1, setsum x1 x2 leaving 2 subgoals.

The subproof is completed by applying H0.

Let x3 of type ο be given.

Assume H1: ∀ x4 . setsum x1 x2 = setsum x1 x4 ⟶ x3.

Apply H1 with x2.

Let x4 of type ι → ι → ο be given.

Assume H2: x4 (setsum x1 x2) (setsum x1 x2).

The subproof is completed by applying H2.

■

Proofgold Proof