let n be Element of NAT ; :: thesis: Decomp (n,1) =
consider A being finite Subset of () such that
A1: Decomp (n,1) = SgmX ((),A) and
A2: for p being Element of 1 -tuples_on NAT holds
( p in A iff Sum p = n ) by Def4;
A3: A =
proof
thus A c= :: according to XBOOLE_0:def 10 :: thesis: c= A
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in A or y in )
assume A4: y in A ; :: thesis: y in
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 ;
hence y in by ; :: thesis: verum
end;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in or y in A )
assume y in ; :: 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;
len (Decomp (n,1)) = 1 by Th8;
then A8: dom (Decomp (n,1)) = Seg 1 by FINSEQ_1:def 3
.= dom by FINSEQ_1:38 ;
field () = 1 -tuples_on NAT by ORDERS_1:15;
then TuplesOrder 1 linearly_orders A by ;
then ( rng = & rng (Decomp (n,1)) = ) by ;
hence Decomp (n,1) = by ; :: thesis: verum