theorem :: VALUED_2:39

for c being Complex
for g, h being complex-valued Function holds (g (#) h) (/) c = g (#) (h (/) c)