:: deftheorem defines delneg FINSEQ_9:def 1 :
for f being complex-valued Function holds delneg f = (1 / 2) (#) (f + (abs f));