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

proof

assume k1 >= n ; :: thesis: contradiction
then A9: k2 > n by A6, XXREAL_0:2;
Sum <*k2,(n -' k2)*> = k2 + (n -' k2) by RVSUM_1:107;
then Sum <*k2,(n -' k2)*> >= k2 by NAT_1:11;
then not (Decomp n,2) . (i + 1) in rng (Decomp n,2) by A2, A3, A5, A9;
then not i + 1 in dom (Decomp n,2) by FUNCT_1:def 5;
hence contradiction by A5, 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 A2, A3;
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 A4, A11, Th11;
then i + 1 <= k by NAT_1:13;
hence contradiction by A5, A8, A11, Th11; :: thesis: verum