let X be non empty set ; :: thesis: for f being PartFunc of X,REAL st ( for x being object st x in dom f holds
f . x <= 0 ) holds
f is nonpositive
let f be PartFunc of X,REAL; :: thesis: ( ( for x being object st x in dom f holds
f . x <= 0 ) implies f is nonpositive )
assume A1: for x being object st x in dom f 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 object st
( x in dom f & y = f . x ) by FUNCT_1:def 3;
hence y <= 0 by A1; :: thesis: verum