theorem S2: :: NEWTON04:34
for f being FinSequence of COMPLEX
for n being Nat holds Sum ((f /^ n) | 1) = f . (n + 1)