theorem DNP: :: FINSEQ_9:23

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