theorem :: RVSUM_2:43

for c being Complex
for F being complex-valued FinSequence holds Product (<*c*> ^ F) = c * (Product F)