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

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

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

then A10:
k1 + 1 <= n
by NAT_1:13;
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 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

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