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

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

hence
abs f = f
by A1, PARTFUN1:5; :: thesis: verum(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;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