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 ;
reconsider p1 = p as FinSequence of REAL by ;
A10: (Sum (p | i)) + (p . (i + 1)) >= (Sum (p | i)) + k1 by ;
A11: (Sum (p | j)) + (p . (j + 1)) >= (Sum (p | j)) + k2 by ;
per cases ( i < j or i >= j ) ;
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 ;
then A12: Sum (p | j) >= (Sum (p | j)) + k2 by ;
(Sum (p | j)) + k2 >= Sum (p | j) by NAT_1:11;
then Sum (p | j) = (Sum (p | j)) + k2 by ;
then k2 = 0 ;
hence contradiction by A4; :: thesis: verum
end;
suppose i >= j ; :: thesis: contradiction
then j < i by ;
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 ;
then A13: Sum (p | i) >= (Sum (p | i)) + k1 by ;
(Sum (p | i)) + k1 >= Sum (p | i) by NAT_1:11;
then Sum (p | i) = (Sum (p | i)) + k1 by ;
then k1 = 0 ;
hence contradiction by A3; :: thesis: verum
end;
end;