let i, n, k1, k2 be Element of NAT ; :: thesis: ( (Decomp (n,2)) . i = <*k1,(n -' k1)*> & (Decomp (n,2)) . (i + 1) = <*k2,(n -' k2)*> implies k2 = k1 + 1 )
assume that
A1: (Decomp (n,2)) . i = <*k1,(n -' k1)*> and
A2: (Decomp (n,2)) . (i + 1) = <*k2,(n -' k2)*> ; :: thesis: k2 = k1 + 1
assume A3: k2 <> k1 + 1 ; :: thesis: contradiction
i + 0 < i + 1 by XREAL_1:6;
then A4: k1 < k2 by A1, A2, Th11;
then k1 + 1 <= k2 by NAT_1:13;
then A5: k1 + 1 < k2 by A3, XXREAL_0:1;
consider A being finite Subset of (2 -tuples_on NAT) such that
A6: Decomp (n,2) = SgmX ((TuplesOrder 2),A) and
A7: 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 TuplesOrder 2 linearly_orders A by ORDERS_1:37, ORDERS_1:38;
then A8: rng (Decomp (n,2)) = A by A6, PRE_POLY:def 2;
k1 < n

proof

Sum <*k2,(n -' k2)*> = k2 + (n -' k2) by RVSUM_1:77;
then A9: Sum <*k2,(n -' k2)*> >= k2 by NAT_1:11;
assume k1 >= n ; :: thesis: contradiction
then k2 > n by A4, XXREAL_0:2;
then not (Decomp (n,2)) . (i + 1) in rng (Decomp (n,2)) by A7, A8, A2, A9;
then not i + 1 in dom (Decomp (n,2)) by FUNCT_1:def 3;
hence contradiction by A2, FUNCT_1:def 2; :: thesis: verum

end;

then A10: k1 + 1 <= n by NAT_1:13;
Sum <*(k1 + 1),(n -' (k1 + 1))*> = (k1 + 1) + (n -' (k1 + 1)) by RVSUM_1:77
.= n by A10, XREAL_1:235 ;
then <*(k1 + 1),(n -' (k1 + 1))*> in rng (Decomp (n,2)) by A7, A8;
then consider k being Nat such that
k in dom (Decomp (n,2)) and
A11: (Decomp (n,2)) . k = <*(k1 + 1),(n -' (k1 + 1))*> by FINSEQ_2:10;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
k1 + 0 < k1 + 1 by XREAL_1:6;
then i < k by A1, A11, Th11;
then i + 1 <= k by NAT_1:13;
hence contradiction by A2, A5, A11, Th11; :: thesis: verum