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)

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A3: x in A ; :: thesis:
then reconsider p = x as Element of i -tuples_on NAT ;
A4: Sum p = n by A1, A3;
rng p c= n + 1

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume that
A5: y in rng p and
A6: not y in n + 1 ; :: thesis:
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:

end;

end;

reconsider A = A as finite Subset of (i -tuples_on NAT) by A2;
take SgmX ((TuplesOrder i),A) ; :: thesis:
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: