let X be non empty set ; :: thesis: for f being nonnegative PartFunc of X,ExtREAL holds f = max+ f

let f be nonnegative PartFunc of X,ExtREAL; :: thesis: f = max+ f

b3: dom f = dom (max+ f) by MESFUNC2:def 2;

for x being Element of X st x in dom f holds

f . x = (max+ f) . x

let f be nonnegative PartFunc of X,ExtREAL; :: thesis: f = max+ f

b3: dom f = dom (max+ f) by MESFUNC2:def 2;

for x being Element of X st x in dom f holds

f . x = (max+ f) . x

proof

hence
f = max+ f
by b3, PARTFUN1:5; :: thesis: verum
let x be Element of X; :: thesis: ( x in dom f implies f . x = (max+ f) . x )

assume b2: x in dom f ; :: thesis: f . x = (max+ f) . x

max ((f . x),0) = f . x by SUPINF_2:51, XXREAL_0:def 10;

hence f . x = (max+ f) . x by b2, b3, MESFUNC2:def 2; :: thesis: verum

end;assume b2: x in dom f ; :: thesis: f . x = (max+ f) . x

max ((f . x),0) = f . x by SUPINF_2:51, XXREAL_0:def 10;

hence f . x = (max+ f) . x by b2, b3, MESFUNC2:def 2; :: thesis: verum