theorem :: FINSEQ_9:27

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