theorem S1: :: NEWTON04:33

for f being FinSequence of COMPLEX holds Sum (f | 1) = f . 1