now :: thesis: for f being nonpositive Function of X,ExtREAL holds f is V184()

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

end;

hence for b₁ being Function of X,ExtREAL st b₁ is nonpositive holds
b₁ is V184() ; :: thesis: verum