theorem Th26: :: MATRIXC1:28
for F being FinSequence of COMPLEX
for a being Element of COMPLEX holds Sum (a * F) = a * (Sum F)