theorem :: RVSUM_2:47

for i being Nat
for c1, c2 being Complex holds Product (i |-> (c1 * c2)) = (Product (i |-> c1)) * (Product (i |-> c2))