let f be complex-valued Function; :: thesis: f = (delneg f) - (delpos f)
( dom (delneg f) = dom f & dom (delpos f) = dom f ) by DMN;
then A1: dom f = (dom (delneg f)) /\ (dom (delpos f))
.= dom ((delneg f) - (delpos f)) by VALUED_1:12 ;
for x being object st x in dom f holds
((delneg f) . x) - ((delpos f) . x) = f . x by VAL;
hence f = (delneg f) - (delpos f) by A1, VALUED_1:14; :: thesis: verum