theorem :: AFINSQ_2:64

for cF being complex-valued XFinSequence
for c being Complex holds c * (Sum cF) = Sum (c (#) cF)