theorem :: VALUED_2:36
for c1, c2 being Complex
for g being complex-valued Function holds (g (/) c1) (/) c2 = g (/) (c1 * c2)