let X be set ; :: thesis: for f being PartFunc of X,REAL st ( for x being object st x in dom f holds
0 <= f . x ) holds
f is nonnegative
let f be PartFunc of X,REAL; :: thesis: ( ( for x being object st x in dom f holds
0 <= f . x ) implies f is nonnegative )
assume A1: for x being object st x in dom f holds
0 <= f . x ; :: thesis: f is nonnegative
let y be ExtReal; :: according to SUPINF_2:def 9,SUPINF_2:def 11 :: thesis: ( not y in rng f or 0. <= y )
assume y in rng f ; :: thesis: 0. <= y
then ex x being object st
( x in dom f & y = f . x ) by FUNCT_1:def 3;
hence 0. <= y by A1; :: thesis: verum