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

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

assume f is nonpositive ; :: thesis: for x being set holds f . x <= 0
then A1: rng f is nonpositive by MESFUNC5:def 2;

hereby :: thesis: verum

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

now

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

end;

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

end;

end;

assume A3: for x being set holds f . x <= 0 ; :: thesis: f is nonpositive
let y be R_eal; :: according to MESFUNC5:def 1,MESFUNC5:def 2 :: thesis: ( not y in rng f or y <= 0 )
assume y in rng f ; :: thesis: y <= 0
then ex x being set st
( x in dom f & y = f . x ) by FUNCT_1:def 3;
hence y <= 0 by A3; :: thesis: verum