theorem :: NEWTON04:30

for f being complex-valued FinSequence
for x being Complex holds Sum (f - x) = (Sum f) - (x * (len f))