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

x in dom (f (#) f) and

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

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

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

set R = f (#) f;

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

then consider x being object such that

x in dom (f (#) f) and

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

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

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