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 4;
then A4: (Decomp (n,2)) . j = (Decomp (n,2)) /. j by PARTFUN1:def 8;
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:100;
then A6: TuplesOrder 2 linearly_orders A by ORDERS_1:133, ORDERS_1:134;
A7: i in dom (Decomp (n,2)) by A1, FUNCT_1:def 4;
then A8: (Decomp (n,2)) . i = (Decomp (n,2)) /. i by PARTFUN1:def 8;
thus ( i < j implies k1 < k2 ) :: thesis: ( k1 < k2 implies i < j )

proof

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, Def2;
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 Element of NAT st 1 <= k & k < t holds
<*k1,(n -' k1)*> . k = <*k2,(n -' k2)*> . k by Def1;

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

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

then <*k1,(n -' k1)*> . t = k1 by FINSEQ_1:61;
hence k1 < k2 by A12, A14, FINSEQ_1:61; :: thesis: verum

end;

suppose t = 2 ; :: thesis: k1 < k2

then <*k1,(n -' k1)*> . 1 = <*k2,(n -' k2)*> . 1 by A13;
then <*k1,(n -' k1)*> . 1 = k2 by FINSEQ_1:61;
then k1 = k2 by FINSEQ_1:61;
hence k1 < k2 by A12; :: thesis: verum

end;

end;

end;

assume A15: k1 < k2 ; :: thesis: i < j
A16: for k being Element of NAT st 1 <= k & k < 1 holds
<*k1,(n -' k1)*> . k = <*k2,(n -' k2)*> . k ;
A17: <*k1,(n -' k1)*> . 1 = k1 by FINSEQ_1:61;
( 1 in Seg 2 & <*k2,(n -' k2)*> . 1 = k2 ) by FINSEQ_1:3, FINSEQ_1:61;
then A18: <*k1,(n -' k1)*> < <*k2,(n -' k2)*> by A15, A17, A16, Def1;
assume A19: i >= j ; :: thesis: contradiction

per cases ( i = j or j < i ) by A19, XXREAL_0:1;

suppose i = j ; :: thesis: contradiction

hence contradiction by A1, A2, A15, A17, FINSEQ_1:61; :: thesis: verum

end;

suppose A20: j < i ; :: thesis: contradiction

then [<*k2,(n -' k2)*>,<*k1,(n -' k1)*>] in TuplesOrder 2 by A5, A6, A1, A2, A7, A3, A8, A4, PRE_POLY:def 2;
then A21: <*k2,(n -' k2)*> <= <*k1,(n -' k1)*> by Def3;
<*k2,(n -' k2)*> <> <*k1,(n -' k1)*> by A5, A6, A1, A2, A7, A3, A8, A4, A20, PRE_POLY:def 2;
hence contradiction by A18, A21, Def2; :: thesis: verum

end;

end;