theorem S2: :: NEWTON04:34

for f being complex-valued FinSequence
for n being Nat holds Sum ((f /^ n) | 1) = f . (n + 1)