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 )
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;
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;
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;
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:44;
then k1 = k2 by FINSEQ_1:44;
hence k1 < k2 by A12; :: thesis: verum
end;
end;
end;
assume A15: k1 < k2 ; :: thesis: 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
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:44; :: thesis: verum
end;
suppose 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 A20: <*k2,(n -' k2)*> <= <*k1,(n -' k1)*> by Def3;
thus contradiction by A18, A20; :: thesis: verum
end;
end;