Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Apply unknownprop_390fca52cd547a01287e1b72ed6b3adcf1f85df24d75a2f5e1a912006e833a34 with λ x3 x4 : ι → ι → ι . In x2 (x4 x0 x1) ⟶ In (setsum x1 x2) x0.

Assume H0: In x2 (ReplSep x0 (λ x3 . ∃ x4 . x3 = setsum x1 x4) (λ x3 . proj1 x3)).

Apply unknownprop_021a576837934491f6aaf936d4c5a9c68d45f2b77fcd13cc395cfdeec72f7dac with x0, λ x3 . ∃ x4 . x3 = setsum x1 x4, proj1, x2, In (setsum x1 x2) x0 leaving 2 subgoals.

The subproof is completed by applying H0.

Let x3 of type ι be given.

Assume H1: In x3 x0.

Assume H2: ∃ x4 . x3 = setsum x1 x4.

Assume H3: x2 = proj1 x3.

Apply H2 with In (setsum x1 x2) x0.

Let x4 of type ι be given.

Assume H4: x3 = setsum x1 x4.

Claim L5: x2 = x4

Apply H3 with λ x5 x6 . x6 = x4.

Apply H4 with λ x5 x6 . proj1 x6 = x4.

The subproof is completed by applying unknownprop_d4bb68cbfba730ad1b1ee2c6901fadf3c573cb615fac3296f9bb52128e37668a with x1, x4.

Claim L6: x3 = setsum x1 x2

Apply L5 with λ x5 x6 . x3 = setsum x1 x6.

The subproof is completed by applying H4.

Apply L6 with λ x5 x6 . In x5 x0.

The subproof is completed by applying H1.

■

Proofgold Proof