for r being Real st r in rng (a (#) b) holds
0 <= r

proof

let r be Real; :: thesis: ( r in rng (a (#) b) implies 0 <= r )
assume r in rng (a (#) b) ; :: thesis: 0 <= r
then consider x being object such that
AS1: ( x in dom (a (#) b) & r = (a (#) b) . x ) by FUNCT_1:def 3;
x in (dom a) /\ (dom b) by AS1, VALUED_1:def 4;
then ( x in dom a & x in dom b ) by XBOOLE_0:def 4;
then ( a . x in rng a & b . x in rng b ) by FUNCT_1:3;
then L1: ( 0 <= a . x & 0 <= b . x ) by PARTFUN3:def 4;
(a (#) b) . x = (a . x) * (b . x) by AS1, VALUED_1:def 4;
hence 0 <= r by L1, AS1; :: thesis: verum

end;

hence a (#) b is nonnegative-yielding ; :: thesis: verum