for r being Real st r in rng ((a,b) In_Power n) holds
r >= 0
proof
let r be Real; :: thesis: ( r in rng ((a,b) In_Power n) implies r >= 0 )
assume B1: r in rng ((a,b) In_Power n) ; :: thesis: r >= 0
ex k being object st
( k in dom ((a,b) In_Power n) & r = ((a,b) In_Power n) . k ) by B1, FUNCT_1:def 3;
hence r >= 0 ; :: thesis: verum
end;
hence (a,b) In_Power n is nonnegative-yielding by PARTFUN3:def 4; :: thesis: verum