Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Let x2 of type ι be given.
Assume H0:
x2 ∈ lam x0 (λ x3 . x1 x3).
Apply lamE with
x0,
x1,
x2,
∃ x3 . and (x3 ∈ x0) (∃ x4 . x2 = setsum x3 x4) leaving 2 subgoals.
The subproof is completed by applying H0.
Let x3 of type ι be given.
Assume H1:
(λ x4 . and (x4 ∈ x0) (∃ x5 . and (x5 ∈ x1 x4) (x2 = setsum x4 x5))) x3.
Apply H1 with
∃ x4 . and (x4 ∈ x0) (∃ x5 . x2 = setsum x4 x5).
Assume H2: x3 ∈ x0.
Assume H3:
∃ x4 . and (x4 ∈ x1 x3) (x2 = setsum x3 x4).
Apply H3 with
∃ x4 . and (x4 ∈ x0) (∃ x5 . x2 = setsum x4 x5).
Let x4 of type ι be given.
Assume H4:
(λ x5 . and (x5 ∈ x1 x3) (x2 = setsum x3 x5)) x4.
Apply H4 with
∃ x5 . and (x5 ∈ x0) (∃ x6 . x2 = setsum x5 x6).
Assume H5: x4 ∈ x1 x3.
Let x5 of type ο be given.
Assume H7:
∀ x6 . and (x6 ∈ x0) (∃ x7 . x2 = setsum x6 x7) ⟶ x5.
Apply H7 with
x3.
Apply andI with
x3 ∈ x0,
∃ x6 . x2 = setsum x3 x6 leaving 2 subgoals.
The subproof is completed by applying H2.
Let x6 of type ο be given.
Assume H8:
∀ x7 . x2 = setsum x3 x7 ⟶ x6.
Apply H8 with
x4.
The subproof is completed by applying H6.