reconsider n1 = n + 1 as non empty set ;
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();
A2: A c= i -tuples_on (n + 1)

proof

let x be object ; :: 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;
rng p c= n + 1

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng p or y in n + 1 )
assume that
A5: y in rng p and
A6: 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 A5;
not y in { t where t is Nat : t < n + 1 } by A6, AXIOMS:4;
then A7: k >= n + 1 ;
ex j being Nat st
( j in dom p & p . j = k ) by A5, FINSEQ_2:10;
then Sum p >= k by Th4;
hence contradiction by A4, A7, NAT_1:13; :: thesis: verum

end;

then ( len p = i & p is FinSequence of n + 1 ) by CARD_1:def 7, FINSEQ_1:def 4;
then p is Element of i -tuples_on n1 by FINSEQ_2:92;
hence x in i -tuples_on (n + 1) ; :: thesis: verum

end;

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