set f = the PartFunc of X,ExtREAL;
take |. the PartFunc of X,ExtREAL.| ; :: thesis: |. the PartFunc of X,ExtREAL.| is nonnegative

now :: thesis: for x being object st x in dom |. the PartFunc of X,ExtREAL.| holds
0. <= |. the PartFunc of X,ExtREAL.| . x

let x be object ; :: thesis: ( x in dom |. the PartFunc of X,ExtREAL.| implies 0. <= |. the PartFunc of X,ExtREAL.| . x )
assume x in dom |. the PartFunc of X,ExtREAL.| ; :: thesis: 0. <= |. the PartFunc of X,ExtREAL.| . x
then |. the PartFunc of X,ExtREAL.| . x = |.( the PartFunc of X,ExtREAL . x).| by MESFUNC1:def 10;
hence 0. <= |. the PartFunc of X,ExtREAL.| . x by EXTREAL1:14; :: thesis: verum

end;

hence |. the PartFunc of X,ExtREAL.| is nonnegative by SUPINF_2:52; :: thesis: verum