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

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

assume f is nonnegative ; :: thesis: for x being set holds 0 <= f . x
then A1: rng f is nonnegative by SUPINF_2:def 22;

hereby :: thesis: verum

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

now

assume x in dom f ; :: thesis: 0 <= f . x
then A2: f . x in rng f by FUNCT_1:def 5;
f . x in REAL ;
hence 0 <= f . x by A1, A2, NUMBERS:31, SUPINF_2:def 15; :: thesis: verum

end;

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

end;

end;

assume A3: for x being set holds 0 <= f . x ; :: thesis: f is nonnegative
let y be R_eal; :: according to SUPINF_2:def 15,SUPINF_2:def 22 :: thesis: ( not y in rng f or 0. <= y )
assume y in rng f ; :: thesis: 0. <= y
then ex x being set st
( x in dom f & y = f . x ) by FUNCT_1:def 5;
hence 0. <= y by A3; :: thesis: verum