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 b1 being Function of X,ExtREAL st b1 is nonpositive holds
b1 is V184() ; :: thesis: verum