for F being FinSequence of COMPLEX
for a being Element of COMPLEX holds Sum (a * F) = a * (Sum F)