theorem S1: :: NEWTON04:33

for f being complex-valued FinSequence holds Sum (f | 1) = f . 1