theorem DNF: :: FINSEQ_9:28

for f being complex-valued Function holds delneg f = delpos (- f)