let X be set ; :: thesis: for F being PartFunc of X,ExtREAL holds

( F is nonpositive iff for n being object holds F . n <= 0. )

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

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 object st

( x in dom F & y = F . x ) by FUNCT_1:def 3;

hence y <= 0 by A2; :: thesis: verum

( F is nonpositive iff for n being object holds F . n <= 0. )

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

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

assume A2:
for n being object holds F . n <= 0.
; :: thesis: F is nonpositive assume
F is nonpositive
; :: thesis: for n being object holds F . b_{2} <= 0.

then A1: rng F is nonpositive ;

let n be object ; :: thesis: F . b_{1} <= 0.

end;then A1: rng F is nonpositive ;

let n be object ; :: thesis: F . b

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 object st

( x in dom F & y = F . x ) by FUNCT_1:def 3;

hence y <= 0 by A2; :: thesis: verum