let f be complex-valued Function; :: thesis: abs f = (delneg f) + (delpos f)
reconsider fabs = abs f as dom f -defined complex-valued Function ;
reconsider g = (1 / 2) (#) f as dom f -defined complex-valued Function ;
reconsider h = g - g as empty-yielding dom f -defined total Function ;
(delneg f) + (delpos f) = (((1 / 2) (#) fabs) + ((1 / 2) (#) f)) + ((1 / 2) (#) (fabs - f)) by RFUNCT_1:16
.= (((1 / 2) (#) fabs) + ((1 / 2) (#) f)) + (((1 / 2) (#) fabs) - ((1 / 2) (#) f)) by RFUNCT_1:18
.= ((((1 / 2) (#) fabs) + ((1 / 2) (#) f)) + ((1 / 2) (#) fabs)) - ((1 / 2) (#) f) by RFUNCT_1:23
.= (((1 / 2) (#) f) + (((1 / 2) (#) fabs) + ((1 / 2) (#) fabs))) - ((1 / 2) (#) f) by RFUNCT_1:8
.= (((1 / 2) (#) f) - ((1 / 2) (#) f)) + (((1 / 2) (#) fabs) + ((1 / 2) (#) fabs)) by RFUNCT_1:23
.= (((1 / 2) (#) f) - ((1 / 2) (#) f)) + (((1 / 2) + (1 / 2)) (#) fabs) by TOPREALC:2
.= fabs ;
hence abs f = (delneg f) + (delpos f) ; :: thesis: verum