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;

A3: A = {<*n*>}

then A8: dom (Decomp (n,1)) = Seg 1 by FINSEQ_1:def 3

.= dom <*<*n*>*> by FINSEQ_1:38 ;

field (TuplesOrder 1) = 1 -tuples_on NAT by ORDERS_1:15;

then TuplesOrder 1 linearly_orders A by ORDERS_1:37, ORDERS_1:38;

then ( rng <*<*n*>*> = {<*n*>} & rng (Decomp (n,1)) = {<*n*>} ) by A1, A3, FINSEQ_1:39, PRE_POLY:def 2;

hence Decomp (n,1) = <*<*n*>*> by A8, FUNCT_1:7; :: thesis: verum

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

len (Decomp (n,1)) = 1
by Th8;
thus
A c= {<*n*>}
:: according to XBOOLE_0:def 10 :: thesis: {<*n*>} c= 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;proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in {<*n*>} or y in A )
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;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

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

then A8: dom (Decomp (n,1)) = Seg 1 by FINSEQ_1:def 3

.= dom <*<*n*>*> by FINSEQ_1:38 ;

field (TuplesOrder 1) = 1 -tuples_on NAT by ORDERS_1:15;

then TuplesOrder 1 linearly_orders A by ORDERS_1:37, ORDERS_1:38;

then ( rng <*<*n*>*> = {<*n*>} & rng (Decomp (n,1)) = {<*n*>} ) by A1, A3, FINSEQ_1:39, PRE_POLY:def 2;

hence Decomp (n,1) = <*<*n*>*> by A8, FUNCT_1:7; :: thesis: verum