let p be FinSequence of NAT ; for i, j, k1, k2 being Element of NAT st i < len p & j < len p & 1 <= k1 & 1 <= k2 & k1 <= p . (i + 1) & k2 <= p . (j + 1) & (Sum (p | i)) + k1 = (Sum (p | j)) + k2 holds
( i = j & k1 = k2 )
let i, j, k1, k2 be Element of NAT ; ( i < len p & j < len p & 1 <= k1 & 1 <= k2 & k1 <= p . (i + 1) & k2 <= p . (j + 1) & (Sum (p | i)) + k1 = (Sum (p | j)) + k2 implies ( i = j & k1 = k2 ) )
assume that
A1:
i < len p
and
A2:
j < len p
and
A3:
1 <= k1
and
A4:
1 <= k2
and
A5:
k1 <= p . (i + 1)
and
A6:
k2 <= p . (j + 1)
and
A7:
(Sum (p | i)) + k1 = (Sum (p | j)) + k2
and
A8:
( i <> j or k1 <> k2 )
; contradiction
A9:
i <> j
by A7, A8, XCMPLX_1:2;
reconsider p1 = p as FinSequence of REAL by FINSEQ_2:24, NUMBERS:19;
A10:
(Sum (p | i)) + (p . (i + 1)) >= (Sum (p | i)) + k1
by A5, XREAL_1:6;
A11:
(Sum (p | j)) + (p . (j + 1)) >= (Sum (p | j)) + k2
by A6, XREAL_1:6;