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 )
A1: dom f = dom (abs f) by VALUED_1:def 11;
assume A2: f is nonnegative ; :: thesis: abs f = f
now :: thesis: for x being Element of X st x in dom f holds
(abs f) . x = f . x
let x be Element of X; :: thesis: ( x in dom f implies (abs f) . x = f . x )
A3: f . x >= 0 by A2, 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 = |.(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 A1, PARTFUN1:5; :: thesis: verum