let X be non empty set ; :: thesis: for f being PartFunc of X,REAL st f is nonnegative holds
abs f = f
let f be PartFunc of X,REAL ; :: thesis: ( f is nonnegative implies abs f = f )
A2: dom f = dom (abs f) by VALUED_1:def 11;
assume A1: f is nonnegative ; :: thesis: abs f = f

now

let x be Element of X; :: thesis: ( x in dom f implies (abs f) . x = f . x )
A3: f . x >= 0 by A1, MESFUNC6:51;
assume x in dom f ; :: thesis: (abs f) . x = f . x
then x in dom (abs f) by VALUED_1:def 11;
then (abs f) . x = abs (f . x) by VALUED_1:def 11;
hence (abs f) . x = f . x by A3, ABSVALUE:def 1; :: thesis: verum

end;

hence abs f = f by A2, PARTFUN1:34; :: thesis: verum