now :: thesis: for x being object st x in dom |.f.| holds
0. <= |.f.| . x

let x be object ; :: thesis: ( x in dom |.f.| implies 0. <= |.f.| . x )
assume x in dom |.f.| ; :: thesis: 0. <= |.f.| . x
then |.f.| . x = |.(f . x).| by MESFUNC1:def 10;
hence 0. <= |.f.| . x by EXTREAL1:14; :: thesis: verum

end;

hence for b₁ being PartFunc of X,ExtREAL st b₁ = |.f.| holds
b₁ is nonnegative by SUPINF_2:52; :: thesis: verum