theorem Th10: :: MATRIXJ1:10

for i, j being Nat
for f being FinSequence of NAT st i in dom f & j in Seg (f /. i) holds
( j + (Sum (f | (i -' 1))) in Seg (Sum (f | i)) & min (f,(j + (Sum (f | (i -' 1))))) = i )