theorem FINSEQ1D7: :: NEWTON07:50

for f being FinSequence
for n being Nat holds (f ^ <*0*>) . n = f . n