theorem :: RVSUM_2:23

for c1, c2 being Complex
for F being complex-valued FinSequence holds (c1 + c2) * F = (c1 * F) + (c2 * F)