let y be Real; :: according to PARTFUN3:def 4 :: thesis: ( not y in rng ((- r) (#) f) or 0 <= y )
assume B1: y in rng ((- r) (#) f) ; :: thesis: 0 <= y
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 0 <= y by B2; :: thesis: verum