theorem :: MATRIXJ1:11

for f being FinSequence of NAT
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