let r be Real; :: 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 object such that

x in dom (abs f) and

A1: (abs f) . x = r by FUNCT_1:def 3;

not |.(f . x).| is negative by COMPLEX1:46;

hence 0 <= r by A1, VALUED_1:18; :: thesis: verum

set R = abs f;

assume r in rng (abs f) ; :: thesis: 0 <= r

then consider x being object such that

x in dom (abs f) and

A1: (abs f) . x = r by FUNCT_1:def 3;

not |.(f . x).| is negative by COMPLEX1:46;

hence 0 <= r by A1, VALUED_1:18; :: thesis: verum