let i, n, k1, k2 be Element of NAT ; ( (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)*>
; k2 = k1 + 1
assume A3:
k2 <> k1 + 1
; 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
;
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;
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; verum