theorem Th17: :: LIOUVIL1:17

for f being Real_Sequence
for k, n being Nat st k in Seg n holds
(f |_ (Seg n)) . k = f . k