theorem :: RVSUM_1:106

for i being natural Number
for r1, r2 being Real holds Product (i |-> (r1 * r2)) = (Product (i |-> r1)) * (Product (i |-> r2))