reconsider p2 = (i -' 1) |-> 0 as FinSequence of NAT ;

i >= 1 by NAT_1:14;

then (i -' 1) + 1 = i by XREAL_1:235;

then ((i -' 1) |-> 0) ^ <*n*> is Tuple of i, NAT ;

then reconsider p1 = ((i -' 1) |-> 0) ^ <*n*> as Element of i -tuples_on NAT by FINSEQ_2:131;

consider A being finite Subset of (i -tuples_on NAT) such that

A1: Decomp (n,i) = SgmX ((TuplesOrder i),A) and

A2: for p being Element of i -tuples_on NAT holds

( p in A iff Sum p = n ) by Def4;

Sum p1 = (Sum p2) + n by RVSUM_1:74

.= 0 + n by RVSUM_1:81 ;

then reconsider A = A as non empty finite Subset of (i -tuples_on NAT) by A2;

( not SgmX ((TuplesOrder i),A) is empty & SgmX ((TuplesOrder i),A) is finite ) ;

hence ( not Decomp (n,i) is empty & Decomp (n,i) is one-to-one & Decomp (n,i) is FinSequence-yielding ) by A1; :: thesis: verum

i >= 1 by NAT_1:14;

then (i -' 1) + 1 = i by XREAL_1:235;

then ((i -' 1) |-> 0) ^ <*n*> is Tuple of i, NAT ;

then reconsider p1 = ((i -' 1) |-> 0) ^ <*n*> as Element of i -tuples_on NAT by FINSEQ_2:131;

consider A being finite Subset of (i -tuples_on NAT) such that

A1: Decomp (n,i) = SgmX ((TuplesOrder i),A) and

A2: for p being Element of i -tuples_on NAT holds

( p in A iff Sum p = n ) by Def4;

Sum p1 = (Sum p2) + n by RVSUM_1:74

.= 0 + n by RVSUM_1:81 ;

then reconsider A = A as non empty finite Subset of (i -tuples_on NAT) by A2;

( not SgmX ((TuplesOrder i),A) is empty & SgmX ((TuplesOrder i),A) is finite ) ;

hence ( not Decomp (n,i) is empty & Decomp (n,i) is one-to-one & Decomp (n,i) is FinSequence-yielding ) by A1; :: thesis: verum