(1 / 2) (#) (f + (abs f)) = ((1 / 2) (#) f) + ((1 / 2) (#) f) by RFUNCT_1:16
.= ((1 / 2) + (1 / 2)) (#) f by TOPREALC:2 ;
hence delneg f = f ; :: thesis: verum