let n be Element of NAT ; :: thesis: len (Decomp (n,1)) = 1
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;
A3: A = {<*n*>}

proof

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

proof

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

end;

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

end;

field (TuplesOrder 1) = 1 -tuples_on NAT by ORDERS_1:15;
then TuplesOrder 1 linearly_orders 1 -tuples_on NAT by ORDERS_1:37;
hence len (Decomp (n,1)) = card A by A1, ORDERS_1:38, PRE_POLY:11
.= 1 by A3, CARD_1:30 ;
:: thesis: verum