let X be non empty set ; :: thesis: for f being PartFunc of X,REAL holds abs f is nonnegative
let f be PartFunc of X,REAL; :: thesis: abs f is nonnegative

now

let x be set ; :: thesis: ( x in dom (abs f) implies 0 <= (abs f) . x )
assume x in dom (abs f) ; :: thesis: 0 <= (abs f) . x
then (abs f) . x = abs (f . x) by VALUED_1:def 11;
hence 0 <= (abs f) . x by COMPLEX1:46; :: thesis: verum

end;

hence abs f is nonnegative by MESFUNC6:52; :: thesis: verum