consider f being PartFunc of X,ExtREAL;
take |.f.| ; :: thesis: |.f.| is nonnegative

now

let x be set ; :: 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 EXTREAL2:51; :: thesis: verum

end;

hence |.f.| is nonnegative by SUPINF_2:71; :: thesis: verum