theorem :: RVSUM_1:112

for i, j being natural Number
for z being Element of COMPLEX holds Product ((i * j) |-> z) = Product (j |-> (Product (i |-> z)))