theorem :: VALUED_2:38
for c being Complex
for g, h being complex-valued Function holds (g - h) (/) c = (g (/) c) - (h (/) c)