theorem Th29: :: NEWTON02:127

for m being Nat
for f being FinSequence of REAL
for n being Nat st n in dom f & m in dom ((f | n) /^ 1) holds
((f | n) /^ 1) . m = f . (m + 1)