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

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 & j <= len f & Sum (f | i) = Sum (f | j) ) and
A3: ( ( i in dom f implies f . i <> 0 ) & ( j in dom f implies f . j <> 0 ) ) ; :: thesis: not i > j
assume A4: i > j ; :: thesis: contradiction
then reconsider i1 = i - 1 as Element of NAT by NAT_1:20;
i = i1 + 1 ;
then ( i > i1 & j <= i1 & j in NAT ) by A4, NAT_1:13, ORDINAL1:def 13;
then A5: ( i >= 1 & Sum (f | j) <= Sum (f | i1) ) by NAT_1:14, POLYNOM3:18;
then i in dom f by A2, FINSEQ_3:27;
then f | (i1 + 1) = (f | i1) ^ <*(f . i)*> by FINSEQ_5:11;
then A6: Sum (f | j) = (Sum (f | i1)) + (f . i) by A2, RVSUM_1:104;
then Sum (f | i1) <= Sum (f | j) by NAT_1:11;
then Sum (f | i1) = Sum (f | j) by A5, XXREAL_0:1;
hence contradiction by A3, A5, A6, A2, FINSEQ_3:27; :: 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
A7: ( i <= len f & j <= len f & Sum (f | i) = Sum (f | j) ) and
A8: ( ( i in dom f implies f . i <> 0 ) & ( j in dom f implies f . j <> 0 ) ) ; :: thesis: i = j
( i <= j & j <= i ) by A1, A7, A8;
hence i = j by XXREAL_0:1; :: thesis: verum