:: deftheorem defines - VALUED_1:def 3 :
for f being complex-valued Function
for r being Complex holds f - r = (- r) + f;