let r be real number ; :: according to PARTFUN3:def 4 :: thesis: ( r in rng (abs f) implies 0 <= r )
set R = abs f;
assume r in rng (abs f) ; :: thesis: 0 <= r
then consider x being set such that
x in dom (abs f) and
A1: (abs f) . x = r by FUNCT_1:def 5;
not abs (f . x) is negative by COMPLEX1:132;
hence 0 <= r by A1, VALUED_1:18; :: thesis: verum