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