now :: thesis: for f being nonpositive Function of X,ExtREAL holds f is without+infty

let f be nonpositive Function of X,ExtREAL; :: thesis: f is without+infty
for x being object holds f . x < +infty by MESFUNC5:8;
hence f is without+infty by MESFUNC5:def 6; :: thesis: verum

end;

hence for b₁ being Function of X,ExtREAL st b₁ is nonpositive holds
b₁ is without+infty ; :: thesis: verum