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