let f be real-valued Function; :: thesis: for x being object holds
( f . x = (delneg f) . x or f . x = - ((delpos f) . x) )
let x be object ; :: thesis: ( f . x = (delneg f) . x or f . x = - ((delpos f) . x) )
A2: ( dom (delneg f) = dom f & dom (delpos f) = dom f ) by DMN;

per cases ( not x in dom f or x in dom f ) ;

suppose not x in dom f ; :: thesis: ( f . x = (delneg f) . x or f . x = - ((delpos f) . x) )

then ( f . x = {} & (delneg f) . x = {} & (delpos f) . x = {} ) by A2, FUNCT_1:def 2;
hence ( f . x = (delneg f) . x or f . x = - ((delpos f) . x) ) ; :: thesis: verum

end;

suppose A0: x in dom f ; :: thesis: ( f . x = (delneg f) . x or f . x = - ((delpos f) . x) )

A3: dom (abs f) = dom f by VALUED_1:def 11;
then ( (dom f) /\ (dom (abs f)) = dom f & (dom (abs f)) /\ (dom f) = dom f ) ;
then A4: ( dom (f + (abs f)) = dom f & dom ((abs f) - f) = dom f ) by VALUED_1:def 1, VALUED_1:12;

per cases ( f . x >= 0 or f . x < 0 ) ;

suppose B1: f . x >= 0 ; :: thesis: ( f . x = (delneg f) . x or f . x = - ((delpos f) . x) )

(abs f) . x = |.(f . x).| by A0, A3, VALUED_1:def 11
.= f . x by B1, ABSVALUE:def 1 ;
then f . x = (1 / 2) * ((f . x) + ((abs f) . x))
.= (1 / 2) * ((f + (abs f)) . x) by A0, A4, VALUED_1:def 1
.= ((1 / 2) (#) (f + (abs f))) . x by VALUED_1:def 5, A0, A2 ;
hence ( f . x = (delneg f) . x or f . x = - ((delpos f) . x) ) ; :: thesis: verum

end;

suppose B1: f . x < 0 ; :: thesis: ( f . x = (delneg f) . x or f . x = - ((delpos f) . x) )

(abs f) . x = |.(f . x).| by A0, A3, VALUED_1:def 11
.= - (f . x) by B1, ABSVALUE:def 1 ;
then f . x = - ((1 / 2) * (((abs f) . x) - (f . x)))
.= - ((1 / 2) * (((abs f) - f) . x)) by A0, A4, VALUED_1:13
.= (- 1) * ((1 / 2) * (((abs f) - f) . x))
.= (- 1) * (((1 / 2) (#) ((abs f) - f)) . x) by A0, VALUED_1:def 5, A2 ;
hence ( f . x = (delneg f) . x or f . x = - ((delpos f) . x) ) ; :: thesis: verum

end;

end;

end;

end;