now :: thesis: for f being nonnegative Function of X,ExtREAL holds f is without-infty

let f be nonnegative Function of X,ExtREAL; :: thesis: f is without-infty
for x being object holds f . x > -infty by SUPINF_2:51;
hence f is without-infty by MESFUNC5:def 5; :: thesis: verum

end;

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