theorem :: RVSUM_2:25

for F being complex-valued FinSequence holds mlt ((<*> COMPLEX),F) = <*> COMPLEX