theorem :: RVSUM_1:111

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