let f be FinSequence of NAT ; :: thesis: for i, j being Nat st i <= len f & j <= len f & Sum (f | i) = Sum (f | j) & ( i in dom f implies f . i <> 0 ) & ( j in dom f implies f . j <> 0 ) holds
i = j

A1: now :: thesis: for i, j being Nat st i <= len f & j <= len f & Sum (f | i) = Sum (f | j) & ( i in dom f implies f . i <> 0 ) & ( j in dom f implies f . j <> 0 ) holds
not i > j

let i, j be Nat; :: thesis: ( i <= len f & j <= len f & Sum (f | i) = Sum (f | j) & ( i in dom f implies f . i <> 0 ) & ( j in dom f implies f . j <> 0 ) implies not i > j )
assume that
A2: i <= len f and
j <= len f and
A3: Sum (f | i) = Sum (f | j) and
A4: ( i in dom f implies f . i <> 0 ) and
( j in dom f implies f . j <> 0 ) ; :: thesis: not i > j
assume A5: i > j ; :: thesis: contradiction
then reconsider i1 = i - 1 as Element of NAT by NAT_1:20;
A6: i = i1 + 1 ;
then j <= i1 by A5, NAT_1:13;
then A7: Sum (f | j) <= Sum (f | i1) by POLYNOM3:18;
A8: i >= 1 by A6, NAT_1:14;
then i in dom f by A2, FINSEQ_3:25;
then f | (i1 + 1) = (f | i1) ^ <*(f . i)*> by FINSEQ_5:10;
then A9: Sum (f | j) = (Sum (f | i1)) + (f . i) by A3, RVSUM_1:74;
then Sum (f | i1) <= Sum (f | j) by NAT_1:11;
then Sum (f | i1) = Sum (f | j) by A7, XXREAL_0:1;
hence contradiction by A2, A4, A8, A9, FINSEQ_3:25; :: thesis: verum

end;

let i, j be Nat; :: thesis: ( i <= len f & j <= len f & Sum (f | i) = Sum (f | j) & ( i in dom f implies f . i <> 0 ) & ( j in dom f implies f . j <> 0 ) implies i = j )
assume that
A10: i <= len f and
A11: j <= len f and
A12: Sum (f | i) = Sum (f | j) and
A13: ( i in dom f implies f . i <> 0 ) and
A14: ( j in dom f implies f . j <> 0 ) ; :: thesis: i = j
A15: j <= i by A1, A10, A11, A12, A13, A14;
i <= j by A1, A10, A11, A12, A13, A14;
hence i = j by A15, XXREAL_0:1; :: thesis: verum