theorem :: RVSUM_2:46

for i, j being Nat
for c being Complex holds Product ((i * j) |-> c) = Product (j |-> (Product (i |-> c)))