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