:: deftheorem defines (/) VALUED_2:def 32 :
for f being complex-valued Function
for c being Complex holds f (/) c = (1 / c) (#) f;