let p be natural-valued FinSequence; :: thesis: for i, j, k1, k2 being 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 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 NAT by FINSEQ_1:103;
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 ) ;

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;

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;

end;