reconsider p2 = (i -' 1) |-> 0 as FinSequence of NAT ;
i >= 1
by NAT_1:14;
then
(i -' 1) + 1 = i
by XREAL_1:237;
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:151;
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:104
.=
0 + n
by RVSUM_1:111
;
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; verum