reconsider n1 = n + 1 as non empty set ;
defpred S1[ Element of i -tuples_on NAT] means Sum \$1 = n;
consider A being Subset of () such that
A1: for p being Element of i -tuples_on NAT holds
( p in A iff S1[p] ) from 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 ;
then A7: k >= n + 1 ;
ex j being Nat st
( j in dom p & p . j = k ) by ;
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 ;
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 () by A2;
take SgmX ((),A) ; :: thesis: ex A being finite Subset of () st
( SgmX ((),A) = SgmX ((),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 () st
( SgmX ((),A) = SgmX ((),A) & ( for p being Element of i -tuples_on NAT holds
( p in A iff Sum p = n ) ) ) by A1; :: thesis: verum