let r be Real; :: according to PARTFUN3:def 4 :: thesis: ( r in rng (f / f) implies 0 <= r )

set R = f / f;

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

then consider x being object such that

A1: ( x in dom (f / f) & (f / f) . x = r ) by FUNCT_1:def 3;

not (f . x) * ((f . x) ") is negative ;

hence 0 <= r by A1, RFUNCT_1:def 1; :: thesis: verum

set R = f / f;

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

then consider x being object such that

A1: ( x in dom (f / f) & (f / f) . x = r ) by FUNCT_1:def 3;

not (f . x) * ((f . x) ") is negative ;

hence 0 <= r by A1, RFUNCT_1:def 1; :: thesis: verum