theorem Th96: :: RVSUM_1:96
for F being complex-valued FinSequence
for r being Complex holds Product (F ^ <*r*>) = (Product F) * r