Apply Inj0_pair_0_eq with
λ x0 x1 : ι → ι . ∀ x2 x3 x4 . x4 ∈ setsum x2 x3 ⟶ or (∃ x5 . and (x5 ∈ x2) (x4 = x0 x5)) (∃ x5 . and (x5 ∈ x3) (x4 = setsum 1 x5)).
Apply Inj1_pair_1_eq with
λ x0 x1 : ι → ι . ∀ x2 x3 x4 . x4 ∈ setsum x2 x3 ⟶ or (∃ x5 . and (x5 ∈ x2) (x4 = Inj0 x5)) (∃ x5 . and (x5 ∈ x3) (x4 = x0 x5)).
The subproof is completed by applying setsum_Inj_inv.