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

now

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

end;

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