theorem :: VALUED_2:29

for c being Complex
for g being complex-valued Function
for x being object holds (g (/) c) . x = (g . x) / c by VALUED_1:6;