let n be Element of NAT ; :: thesis: (Decomp n,2) . 1 = <*0 ,n*>
consider A being finite Subset of (2 -tuples_on NAT ) such that
A1: Decomp n,2 = SgmX (TuplesOrder 2),A and
A2: for p being Element of 2 -tuples_on NAT holds
( p in A iff Sum p = n ) by Def4;
1 <= n + 1 by NAT_1:11;
then 1 in Seg (n + 1) by FINSEQ_1:3;
then 1 in Seg (len (Decomp n,2)) by Th9;
then A3: 1 in dom (Decomp n,2) by FINSEQ_1:def 3;
Sum <*0 ,n*> = 0 + n by RVSUM_1:107;
then A4: <*0 ,n*> in A by A2;
field (TuplesOrder 2) = 2 -tuples_on NAT by ORDERS_1:100;
then A5: TuplesOrder 2 linearly_orders A by ORDERS_1:133, ORDERS_1:134;

now

let y be Element of 2 -tuples_on NAT ; :: thesis: ( y in A implies [<*0 ,n*>,y] in TuplesOrder 2 )
consider d1, d2 being Element of NAT such that
A6: y = <*d1,d2*> by FINSEQ_2:120;
assume y in A ; :: thesis: [<*0 ,n*>,y] in TuplesOrder 2
then Sum <*d1,d2*> = n by A2, A6;
then A7: d1 + d2 = n by RVSUM_1:107;

now

per cases ( d1 = 0 or d1 > 0 ) ;

suppose d1 = 0 ; :: thesis: <*0 ,n*> <= <*d1,d2*>

hence <*0 ,n*> <= <*d1,d2*> by A7; :: thesis: verum

end;

suppose d1 > 0 ; :: thesis: <*0 ,n*> <= <*d1,d2*>

then <*0 ,n*> . 1 < d1 by FINSEQ_1:61;
then A8: <*0 ,n*> . 1 < <*d1,d2*> . 1 by FINSEQ_1:61;
A9: 1 in Seg 2 by FINSEQ_1:3;
for k being Element of NAT st 1 <= k & k < 1 holds
<*0 ,n*> . k = <*d1,d2*> . k ;
then <*0 ,n*> < <*d1,d2*> by A8, A9, Def1;
hence <*0 ,n*> <= <*d1,d2*> by Def2; :: thesis: verum

end;

end;

end;

hence [<*0 ,n*>,y] in TuplesOrder 2 by A6, Def3; :: thesis: verum

end;

then (SgmX (TuplesOrder 2),A) /. 1 = <*0 ,n*> by A4, A5, POLYNOM1:8;
hence (Decomp n,2) . 1 = <*0 ,n*> by A1, A3, PARTFUN1:def 8; :: thesis: verum