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