let f be complex-valued Function; :: thesis: delneg f = delpos (- f)
reconsider g = - f as complex-valued Function ;
(1 / 2) (#) (f + (abs f)) = ((1 / 2) (#) f) + ((1 / 2) (#) (abs f)) by RFUNCT_1:16
.= ((1 / 2) (#) (abs g)) + ((1 / 2) (#) (- g)) by EUCLID:5
.= ((1 / 2) (#) (abs g)) + (- ((1 / 2) (#) g)) by VALUED_2:23
.= ((1 / 2) (#) (abs g)) - ((1 / 2) (#) g) by VALUED_1:def 9 ;
hence delneg f = delpos (- f) by RFUNCT_1:18; :: thesis: verum