theorem :: RVSUM_2:28

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