theorem :: RVSUM_2:38

for c being Complex
for F being complex-valued FinSequence holds Sum (c * F) = c * (Sum F)