let p be FinSequence of NAT ; :: thesis: 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 ; :: thesis: ( 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 ) ; :: thesis: 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;

( i = j & k1 = k2 )

let i, j, k1, k2 be Element of NAT ; :: thesis: ( 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 ) ; :: thesis: 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;

per cases
( i < j or i >= j )
;

end;

suppose
i < j
; :: thesis: contradiction

then
i + 1 <= j
by NAT_1:13;

then Sum (p | j) >= Sum (p | (i + 1)) by Th17;

then Sum (p | j) >= (Sum (p1 | i)) + (p . (i + 1)) by A1, Th19;

then A12: Sum (p | j) >= (Sum (p | j)) + k2 by A7, A10, XXREAL_0:2;

(Sum (p | j)) + k2 >= Sum (p | j) by NAT_1:11;

then Sum (p | j) = (Sum (p | j)) + k2 by A12, XXREAL_0:1;

then k2 = 0 ;

hence contradiction by A4; :: thesis: verum

end;then Sum (p | j) >= Sum (p | (i + 1)) by Th17;

then Sum (p | j) >= (Sum (p1 | i)) + (p . (i + 1)) by A1, Th19;

then A12: Sum (p | j) >= (Sum (p | j)) + k2 by A7, A10, XXREAL_0:2;

(Sum (p | j)) + k2 >= Sum (p | j) by NAT_1:11;

then Sum (p | j) = (Sum (p | j)) + k2 by A12, XXREAL_0:1;

then k2 = 0 ;

hence contradiction by A4; :: thesis: verum

suppose
i >= j
; :: thesis: contradiction

then
j < i
by A9, XXREAL_0:1;

then j + 1 <= i by NAT_1:13;

then Sum (p | i) >= Sum (p | (j + 1)) by Th17;

then Sum (p | i) >= (Sum (p1 | j)) + (p . (j + 1)) by A2, Th19;

then A13: Sum (p | i) >= (Sum (p | i)) + k1 by A7, A11, XXREAL_0:2;

(Sum (p | i)) + k1 >= Sum (p | i) by NAT_1:11;

then Sum (p | i) = (Sum (p | i)) + k1 by A13, XXREAL_0:1;

then k1 = 0 ;

hence contradiction by A3; :: thesis: verum

end;then j + 1 <= i by NAT_1:13;

then Sum (p | i) >= Sum (p | (j + 1)) by Th17;

then Sum (p | i) >= (Sum (p1 | j)) + (p . (j + 1)) by A2, Th19;

then A13: Sum (p | i) >= (Sum (p | i)) + k1 by A7, A11, XXREAL_0:2;

(Sum (p | i)) + k1 >= Sum (p | i) by NAT_1:11;

then Sum (p | i) = (Sum (p | i)) + k1 by A13, XXREAL_0:1;

then k1 = 0 ;

hence contradiction by A3; :: thesis: verum