:: deftheorem defines - VALUED_1:def 9 :
for f1, f2 being complex-valued Function holds f1 - f2 = f1 + (- f2);