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 16;

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 3;
f . x in REAL ;
hence 0 <= f . x by A1, A2, NUMBERS:31, SUPINF_2:def 9; :: thesis: verum

end;

hence 0 <= f . x by FUNCT_1:def 2; :: 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 9,SUPINF_2:def 16 :: 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 3;
hence 0. <= y by A3; :: thesis: verum