now :: thesis: for f being nonnegative Function of X,ExtREAL holds f is V183()
let f be nonnegative Function of X,ExtREAL; :: thesis: f is V183()
for x being object holds f . x > -infty by SUPINF_2:51;
hence f is V183() by MESFUNC5:def 5; :: thesis: verum
end;
hence for b1 being Function of X,ExtREAL st b1 is nonnegative holds
b1 is V183() ; :: thesis: verum