Apply pred_ext_2 with setsum_p, tuple_p 2 leaving 2 subgoals.

Let x0 of type ι be given.

Apply unknownprop_56bd0714abefd533b13603d171a24196c02fb0b6a0af8036287a8ec089f8957d with λ x1 x2 : ι → ο . x2 x0 ⟶ tuple_p 2 x0.

Assume H0: setsum (ap x0 0) (ap x0 1) = x0.

Apply H0 with λ x1 x2 . tuple_p 2 x1.

Apply unknownprop_2c926b240fc658005337215abfdc8124a6f6eea17ba9f4df80d254bab3845972 with λ x1 x2 : ι → ι → ο . x2 2 (setsum (ap x0 0) (ap x0 1)).

Let x1 of type ι be given.

Assume H1: In x1 (setsum (ap x0 0) (ap x0 1)).

Apply unknownprop_976b9ed71c1ec1f277c9c37a01879b51c2de3497fe82149802bec54f853970e6 with ap x0 0, ap x0 1, x1, λ x2 . ∃ x3 . and (In x3 2) (∃ x4 . x2 = setsum x3 x4) leaving 3 subgoals.

The subproof is completed by applying H1.

Let x2 of type ι be given.

Assume H2: In x2 (ap x0 0).

Let x3 of type ο be given.

Assume H3: ∀ x4 . and (In x4 2) (∃ x5 . setsum 0 x2 = setsum x4 x5) ⟶ x3.

Apply H3 with 0.

Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with In 0 2, ∃ x4 . setsum 0 x2 = setsum 0 x4 leaving 2 subgoals.

The subproof is completed by applying unknownprop_7630054952f4bd54be6e25e2e786a4db7b90ee782d6b1031afa63aeb6d55b595.

Let x4 of type ο be given.

Assume H4: ∀ x5 . setsum 0 x2 = setsum 0 x5 ⟶ x4.

Apply H4 with x2.

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

Assume H5: x5 (setsum 0 x2) (setsum 0 x2).

The subproof is completed by applying H5.

Let x2 of type ι be given.

Assume H2: In x2 (ap x0 1).

Let x3 of type ο be given.

Assume H3: ∀ x4 . and (In x4 2) (∃ x5 . setsum 1 x2 = setsum x4 x5) ⟶ x3.

Apply H3 with 1.

Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with In 1 2, ∃ x4 . setsum 1 x2 = setsum 1 x4 leaving 2 subgoals.

The subproof is completed by applying unknownprop_85e7394990c25c8874e39b4ca1ac83bc7d22390df4a86e0ba0fa73d0ca7d5d30.

Let x4 of type ο be given.

Assume H4: ∀ x5 . setsum 1 x2 = setsum 1 x5 ⟶ x4.

Apply H4 with x2.

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

Assume H5: x5 (setsum 1 x2) (setsum 1 x2).

The subproof is completed by applying H5.

Let x0 of type ι be given.

Apply unknownprop_2c926b240fc658005337215abfdc8124a6f6eea17ba9f4df80d254bab3845972 with λ x1 x2 : ι → ι → ο . x2 2 x0 ⟶ setsum_p x0.

Assume H0: (λ x1 x2 . ∀ x3 . In x3 x2 ⟶ ∃ x4 . and (In x4 x1) (∃ x5 . x3 = setsum x4 x5)) 2 x0.

Apply unknownprop_d487a58526bbc92fd727319b81e7119e7f4709a5ed1caa8f3e6f55fbeafb60d0 with x0.

Let x1 of type ι be given.

Assume H1: In x1 x0.

Apply unknownprop_3848cfb1fd522cb609408da39f227a9c05924a24919f21041d0880590b824ef5 with λ x2 . In x2 2, λ x2 . ∃ x3 . x1 = setsum x2 x3, and (setsum_p x1) (In (ap x1 0) 2) leaving 2 subgoals.

Apply H0 with x1.

The subproof is completed by applying H1.

Let x2 of type ι be given.

Assume H2: In x2 2.

Assume H3: ∃ x3 . x1 = setsum x2 x3.

Apply H3 with and (setsum_p x1) (In (ap x1 0) 2).

Let x3 of type ι be given.

Assume H4: x1 = setsum x2 x3.

Apply H4 with λ x4 x5 . and (setsum_p x5) (In (ap x5 0) 2).

...

■

Proofgold Proof