let X be non empty set ; :: thesis: for f being PartFunc of X,ExtREAL st f is nonpositive holds
f is ()
let f be PartFunc of X,ExtREAL; :: thesis: ( f is nonpositive implies f is () )
assume f is nonpositive ; :: thesis: f is ()
then for x being set holds f . x < +infty by Th8;
hence f is () by Def6; :: thesis: verum