let n be Element of NAT ; :: thesis: Decomp n,1 = <*<*n*>*>
consider A being finite Subset of (1 -tuples_on NAT ) such that
A1: Decomp n,1 = SgmX (TuplesOrder 1),A and
A2: for p being Element of 1 -tuples_on NAT holds
( p in A iff Sum p = n ) by Def4;
len (Decomp n,1) = 1 by Th8;
then A3: dom (Decomp n,1) = Seg 1 by FINSEQ_1:def 3
.= dom <*<*n*>*> by FINSEQ_1:55 ;
A4: A = {<*n*>}

proof

thus A c= {<*n*>} :: according to XBOOLE_0:def 10 :: thesis: {<*n*>} c= A

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in A or y in {<*n*>} )
assume A5: y in A ; :: thesis: y in {<*n*>}
then reconsider p = y as Element of 1 -tuples_on NAT ;
A6: Sum p = n by A2, A5;
consider k being Element of NAT such that
A7: p = <*k*> by FINSEQ_2:117;
Sum p = k by A7, RVSUM_1:103;
hence y in {<*n*>} by A6, A7, TARSKI:def 1; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in {<*n*>} or y in A )
assume y in {<*n*>} ; :: thesis: y in A
then A8: y = <*n*> by TARSKI:def 1;
Sum <*n*> = n by RVSUM_1:103;
hence y in A by A2, A8; :: thesis: verum

end;

A9: rng <*<*n*>*> = {<*n*>} by FINSEQ_1:56;
field (TuplesOrder 1) = 1 -tuples_on NAT by ORDERS_1:100;
then TuplesOrder 1 linearly_orders A by ORDERS_1:133, ORDERS_1:134;
then rng (Decomp n,1) = {<*n*>} by A1, A4, TRIANG_1:def 2;
hence Decomp n,1 = <*<*n*>*> by A3, A9, FUNCT_1:17; :: thesis: verum