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:8;
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:100;
then TuplesOrder 2 linearly_orders A by ORDERS_1:133, ORDERS_1:134;
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:107;
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 5;
hence contradiction by A2, FUNCT_1:def 4; :: 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:107
.= n by A10, XREAL_1:237 ;
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:11;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
k1 + 0 < k1 + 1 by XREAL_1:8;
then i < k by A1, A11, Th11;
then i + 1 <= k by NAT_1:13;
hence contradiction by A2, A5, A11, Th11; :: thesis: verum