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;
A3: now :: thesis: for y being Element of 2 -tuples_on NAT st y in A holds
[<*0,n*>,y] in TuplesOrder 2
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
A4: y = <*d1,d2*> by FINSEQ_2:100;
assume y in A ; :: thesis: [<*0,n*>,y] in TuplesOrder 2
then Sum <*d1,d2*> = n by A2, A4;
then A5: d1 + d2 = n by RVSUM_1:77;
now :: thesis: <*0,n*> <= <*d1,d2*>
per cases ( d1 = 0 or d1 > 0 ) ;
suppose d1 = 0 ; :: thesis: <*0,n*> <= <*d1,d2*>
hence <*0,n*> <= <*d1,d2*> by A5; :: thesis: verum
end;
suppose d1 > 0 ; :: thesis: <*0,n*> <= <*d1,d2*>
then <*0,n*> . 1 < d1 by FINSEQ_1:44;
then A6: <*0,n*> . 1 < <*d1,d2*> . 1 by FINSEQ_1:44;
( 1 in Seg 2 & ( for k being Nat st 1 <= k & k < 1 holds
<*0,n*> . k = <*d1,d2*> . k ) ) by FINSEQ_1:1;
then <*0,n*> < <*d1,d2*> by A6;
hence <*0,n*> <= <*d1,d2*> ; :: thesis: verum
end;
end;
end;
hence [<*0,n*>,y] in TuplesOrder 2 by A4, Def3; :: thesis: verum
end;
1 <= n + 1 by NAT_1:11;
then 1 in Seg (n + 1) by FINSEQ_1:1;
then 1 in Seg (len (Decomp (n,2))) by Th9;
then A7: 1 in dom (Decomp (n,2)) by FINSEQ_1:def 3;
field (TuplesOrder 2) = 2 -tuples_on NAT by ORDERS_1:15;
then A8: TuplesOrder 2 linearly_orders A by ORDERS_1:37, ORDERS_1:38;
Sum <*0,n*> = 0 + n by RVSUM_1:77;
then <*0,n*> in A by A2;
then (SgmX ((TuplesOrder 2),A)) /. 1 = <*0,n*> by A8, A3, PRE_POLY:20;
hence (Decomp (n,2)) . 1 = <*0,n*> by A1, A7, PARTFUN1:def 6; :: thesis: verum