let r be Real; :: according to PARTFUN3:def 4 :: thesis: ( not r in rng (f + (abs f)) or 0 <= r )
assume A1: r in rng (f + (abs f)) ; :: thesis: 0 <= r
consider i being object such that
A2: ( i in dom (f + (abs f)) & (f + (abs f)) . i = r ) by A1, FUNCT_1:def 3;
A3: dom (f + (abs f)) = (dom f) /\ (dom (abs f)) by VALUED_1:def 1;
A4: ( |.(f . i).| = f . i or |.(f . i).| = - (f . i) ) by ABSVALUE:1;
(f + (abs f)) . i = (f . i) + ((abs f) . i) by A2, VALUED_1:def 1
.= (f . i) + |.(f . i).| by A2, A3, VALUED_1:def 11 ;
hence 0 <= r by A2, A4; :: thesis: verum