theorem :: RVSUM_1:105

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