let X be set ; :: thesis: for f being PartFunc of X,REAL holds
( f is nonnegative iff for x being object holds 0 <= f . x )
let f be PartFunc of X,REAL; :: thesis: ( f is nonnegative iff for x being object holds 0 <= f . x )

hereby :: thesis: ( ( for x being object holds 0 <= f . x ) implies f is nonnegative )

assume f is nonnegative ; :: thesis: for x being object holds 0 <= f . x
then A1: rng f is nonnegative ;

hereby :: thesis: verum

let x be object ; :: thesis: 0 <= f . x

now :: thesis: ( x in dom f implies 0 <= f . x )

assume x in dom f ; :: thesis: 0 <= f . x
then A2: f . x in rng f by FUNCT_1:def 3;
thus 0 <= f . x by A1, A2; :: thesis: verum

end;

hence 0 <= f . x by FUNCT_1:def 2; :: thesis: verum

end;

end;

assume A3: for x being object 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 A3; :: thesis: verum