theorem :: RVSUM_1:104
for i, j being natural Number
for r being Real holds Product ((i + j) |-> r) = (Product (i |-> r)) * (Product (j |-> r))