theorem Th9: :: NEWTON02:109

for n being Nat
for f being FinSequence of REAL st n in dom f holds
(f | n) . 1 = f . 1