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 r in (rng a) \/ (rng b) by AFINSQ_1:26;
then ( r in rng a or r in rng b ) by XBOOLE_0:def 3;
hence 0 <= r by PARTFUN3:def 4; :: thesis: verum

end;

hence a ^ b is nonnegative-yielding ; :: thesis: verum