theorem CF: :: NEWTON07:49
for n being non zero Nat
for c being Complex
for f being FinSequence holds (<*c*> ^ f) . (n + 1) = f . n