defpred S₁[ Element of i -tuples_on NAT ] means Sum $1 = n;
consider A being Subset of (i -tuples_on NAT ) such that
A1: for p being Element of i -tuples_on NAT holds
( p in A iff S₁[p] ) from SUBSET_1:sch 3();
reconsider n1 = n + 1 as non empty set ;
n + 1 is finite by CARD_1:69;
then A2: i -tuples_on (n + 1) is finite by YELLOW15:2;
A c= i -tuples_on (n + 1)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in i -tuples_on (n + 1) )
assume A3: x in A ; :: thesis: x in i -tuples_on (n + 1)
then reconsider p = x as Element of i -tuples_on NAT ;
A4: Sum p = n by A1, A3;
A5: len p = i by FINSEQ_1:def 18;
rng p c= n + 1

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng p or y in n + 1 )
assume that
A6: y in rng p and
A7: not y in n + 1 ; :: thesis: contradiction
rng p c= NAT by FINSEQ_1:def 4;
then reconsider k = y as Element of NAT by A6;
not y in { t where t is Element of NAT : t < n + 1 } by A7, AXIOMS:30;
then A8: k >= n + 1 ;
consider j being Nat such that
A9: j in dom p and
A10: p . j = k by A6, FINSEQ_2:11;
Sum p >= k by A9, A10, Th4;
hence contradiction by A4, A8, NAT_1:13; :: thesis: verum

end;

then p is FinSequence of n + 1 by FINSEQ_1:def 4;
then p is Element of i -tuples_on n1 by A5, FINSEQ_2:110;
hence x in i -tuples_on (n + 1) ; :: thesis: verum

end;

then reconsider A = A as finite Subset of (i -tuples_on NAT ) by A2;
take SgmX (TuplesOrder i),A ; :: thesis: ex A being finite Subset of (i -tuples_on NAT ) st
( SgmX (TuplesOrder i),A = SgmX (TuplesOrder i),A & ( for p being Element of i -tuples_on NAT holds
( p in A iff Sum p = n ) ) )
thus ex A being finite Subset of (i -tuples_on NAT ) st
( SgmX (TuplesOrder i),A = SgmX (TuplesOrder i),A & ( for p being Element of i -tuples_on NAT holds
( p in A iff Sum p = n ) ) ) by A1; :: thesis: verum