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