reconsider n1 = n + 1 as non empty set ;

defpred S_{1}[ 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_{1}[p] )
from SUBSET_1:sch 3();

A2: A c= i -tuples_on (n + 1)

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

defpred S

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

A2: A c= i -tuples_on (n + 1)

proof

reconsider A = A as finite Subset of (i -tuples_on NAT) by A2;
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

then p is Element of i -tuples_on n1 by FINSEQ_2:92;

hence x in i -tuples_on (n + 1) ; :: thesis: verum

end;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

then
( len p = i & p is FinSequence of n + 1 )
by CARD_1:def 7, FINSEQ_1:def 4;
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;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

then p is Element of i -tuples_on n1 by FINSEQ_2:92;

hence x in i -tuples_on (n + 1) ; :: thesis: verum

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