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