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;

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

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

1 <= n + 1
by NAT_1:11;[<*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;

end;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*>end;

hence
[<*0,n*>,y] in TuplesOrder 2
by A4, Def3; :: thesis: verumper cases
( d1 = 0 or d1 > 0 )
;

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;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

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