let X be set ; :: thesis: for F being PartFunc of X,ExtREAL holds
( F is nonpositive iff for n being set holds F . n <= 0. )
let F be PartFunc of X,ExtREAL ; :: thesis: ( F is nonpositive iff for n being set holds F . n <= 0. )

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

assume F is nonpositive ; :: thesis: for n being set holds F . b₂ <= 0.
then A1: rng F is nonpositive by Def2;
let n be set ; :: thesis: F . b₁ <= 0.

per cases ( n in dom F or not n in dom F ) ;

suppose n in dom F ; :: thesis: F . b₁ <= 0.

then F . n in rng F by FUNCT_1:def 5;
hence F . n <= 0. by A1, Def1; :: thesis: verum

end;

suppose not n in dom F ; :: thesis: F . b₁ <= 0.

hence F . n <= 0. by FUNCT_1:def 4; :: thesis: verum

end;

end;

end;

assume A2: for n being set holds F . n <= 0. ; :: thesis: F is nonpositive
let y be R_eal; :: according to MESFUNC5:def 1,MESFUNC5:def 2 :: thesis: ( y in rng F implies 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 5;
hence y <= 0 by A2; :: thesis: verum