let f be complex-valued Function; :: thesis: ( dom f = dom (delpos f) & dom f = dom (delneg f) & dom f = dom (delall f) )
A1: dom ((1 / 2) (#) (f + (abs f))) = dom (f + (abs f)) by VALUED_1:def 5
.= (dom f) /\ (dom (abs f)) by VALUED_1:def 1
.= dom f by VALUED_1:def 11 ;
dom ((1 / 2) (#) ((abs f) - f)) = dom ((abs f) - f) by VALUED_1:def 5
.= dom ((abs f) + (- f)) by VALUED_1:def 9
.= (dom (- f)) /\ (dom (abs f)) by VALUED_1:def 1
.= (dom ((- 1) (#) f)) /\ (dom (abs f)) by VALUED_1:def 6
.= (dom f) /\ (dom (abs f)) by VALUED_1:def 5
.= dom f by VALUED_1:def 11 ;
hence ( dom f = dom (delpos f) & dom f = dom (delneg f) & dom f = dom (delall f) ) by A1, VALUED_1:def 5; :: thesis: verum