:: deftheorem defines /" VALUED_1:def 10 :
for f1, f2 being complex-valued Function holds f1 /" f2 = f1 (#) (f2 ");