let y be Real; :: according to PARTFUN3:def 3 :: thesis: ( not y in rng ((- r) (#) f) or y <= 0 )
assume B1: y in rng ((- r) (#) f) ; :: thesis: y <= 0
consider x being object such that
B2: ( x in dom ((- r) (#) f) & y = ((- r) (#) f) . x ) by B1, FUNCT_1:def 3;
((- r) (#) f) . x = (- r) * (f . x) by B2, VALUED_1:def 5;
hence y <= 0 by B2; :: thesis: verum