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 b₁ being Function of X,ExtREAL st b₁ is nonnegative holds
b₁ is V183() ; :: thesis: verum