theorem :: RVSUM_1:113

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