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