let i, j, n, k1, k2 be Element of NAT ; :: thesis: ( (Decomp (n,2)) . i = <*k1,(n -' k1)*> & (Decomp (n,2)) . j = <*k2,(n -' k2)*> implies ( i < j iff k1 < k2 ) )

assume that

A1: (Decomp (n,2)) . i = <*k1,(n -' k1)*> and

A2: (Decomp (n,2)) . j = <*k2,(n -' k2)*> ; :: thesis: ( i < j iff k1 < k2 )

A3: j in dom (Decomp (n,2)) by A2, FUNCT_1:def 2;

then A4: (Decomp (n,2)) . j = (Decomp (n,2)) /. j by PARTFUN1:def 6;

consider A being finite Subset of (2 -tuples_on NAT) such that

A5: Decomp (n,2) = SgmX ((TuplesOrder 2),A) and

for p being Element of 2 -tuples_on NAT holds

( p in A iff Sum p = n ) by Def4;

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

then A6: TuplesOrder 2 linearly_orders A by ORDERS_1:37, ORDERS_1:38;

A7: i in dom (Decomp (n,2)) by A1, FUNCT_1:def 2;

then A8: (Decomp (n,2)) . i = (Decomp (n,2)) /. i by PARTFUN1:def 6;

thus ( i < j implies k1 < k2 ) :: thesis: ( k1 < k2 implies i < j )

A16: for k being Nat st 1 <= k & k < 1 holds

<*k1,(n -' k1)*> . k = <*k2,(n -' k2)*> . k ;

A17: <*k1,(n -' k1)*> . 1 = k1 by FINSEQ_1:44;

( 1 in Seg 2 & <*k2,(n -' k2)*> . 1 = k2 ) by FINSEQ_1:1, FINSEQ_1:44;

then A18: <*k1,(n -' k1)*> < <*k2,(n -' k2)*> by A15, A17, A16;

assume A19: i >= j ; :: thesis: contradiction

assume that

A1: (Decomp (n,2)) . i = <*k1,(n -' k1)*> and

A2: (Decomp (n,2)) . j = <*k2,(n -' k2)*> ; :: thesis: ( i < j iff k1 < k2 )

A3: j in dom (Decomp (n,2)) by A2, FUNCT_1:def 2;

then A4: (Decomp (n,2)) . j = (Decomp (n,2)) /. j by PARTFUN1:def 6;

consider A being finite Subset of (2 -tuples_on NAT) such that

A5: Decomp (n,2) = SgmX ((TuplesOrder 2),A) and

for p being Element of 2 -tuples_on NAT holds

( p in A iff Sum p = n ) by Def4;

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

then A6: TuplesOrder 2 linearly_orders A by ORDERS_1:37, ORDERS_1:38;

A7: i in dom (Decomp (n,2)) by A1, FUNCT_1:def 2;

then A8: (Decomp (n,2)) . i = (Decomp (n,2)) /. i by PARTFUN1:def 6;

thus ( i < j implies k1 < k2 ) :: thesis: ( k1 < k2 implies i < j )

proof

assume A15:
k1 < k2
; :: thesis: i < j
assume A9:
i < j
; :: thesis: k1 < k2

then [<*k1,(n -' k1)*>,<*k2,(n -' k2)*>] in TuplesOrder 2 by A5, A6, A1, A2, A7, A3, A8, A4, PRE_POLY:def 2;

then A10: <*k1,(n -' k1)*> <= <*k2,(n -' k2)*> by Def3;

<*k1,(n -' k1)*> <> <*k2,(n -' k2)*> by A5, A6, A1, A2, A7, A3, A8, A4, A9, PRE_POLY:def 2;

then <*k1,(n -' k1)*> < <*k2,(n -' k2)*> by A10;

then consider t being Element of NAT such that

A11: t in Seg 2 and

A12: <*k1,(n -' k1)*> . t < <*k2,(n -' k2)*> . t and

A13: for k being Nat st 1 <= k & k < t holds

<*k1,(n -' k1)*> . k = <*k2,(n -' k2)*> . k ;

end;then [<*k1,(n -' k1)*>,<*k2,(n -' k2)*>] in TuplesOrder 2 by A5, A6, A1, A2, A7, A3, A8, A4, PRE_POLY:def 2;

then A10: <*k1,(n -' k1)*> <= <*k2,(n -' k2)*> by Def3;

<*k1,(n -' k1)*> <> <*k2,(n -' k2)*> by A5, A6, A1, A2, A7, A3, A8, A4, A9, PRE_POLY:def 2;

then <*k1,(n -' k1)*> < <*k2,(n -' k2)*> by A10;

then consider t being Element of NAT such that

A11: t in Seg 2 and

A12: <*k1,(n -' k1)*> . t < <*k2,(n -' k2)*> . t and

A13: for k being Nat st 1 <= k & k < t holds

<*k1,(n -' k1)*> . k = <*k2,(n -' k2)*> . k ;

per cases
( t = 1 or t = 2 )
by A11, FINSEQ_1:2, TARSKI:def 2;

end;

suppose A14:
t = 1
; :: thesis: k1 < k2

then
<*k1,(n -' k1)*> . t = k1
by FINSEQ_1:44;

hence k1 < k2 by A12, A14, FINSEQ_1:44; :: thesis: verum

end;hence k1 < k2 by A12, A14, FINSEQ_1:44; :: thesis: verum

A16: for k being Nat st 1 <= k & k < 1 holds

<*k1,(n -' k1)*> . k = <*k2,(n -' k2)*> . k ;

A17: <*k1,(n -' k1)*> . 1 = k1 by FINSEQ_1:44;

( 1 in Seg 2 & <*k2,(n -' k2)*> . 1 = k2 ) by FINSEQ_1:1, FINSEQ_1:44;

then A18: <*k1,(n -' k1)*> < <*k2,(n -' k2)*> by A15, A17, A16;

assume A19: i >= j ; :: thesis: contradiction