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

proof

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;

hence f = max+ f by b3, PARTFUN1:5; :: thesis: verum