theorem :: RVSUM_1:98

for r being Real
for F being real-valued FinSequence holds Product (<*r*> ^ F) = r * (Product F)