let X be non empty set ; :: thesis: for f being nonpositive PartFunc of X,ExtREAL holds f = - (max- f)
let f be nonpositive PartFunc of X,ExtREAL; :: thesis: f = - (max- f)
b1: dom f = dom (max- f) by MESFUNC2:def 3
.= dom (- (max- f)) by MESFUNC1:def 7 ;
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) = 0 by MESFUNC5:8, XXREAL_0:def 10;
then (max+ f) . x = 0 by b2, b3, MESFUNC2:def 2;
then (max- f) . x = - (f . x) by b2, MESFUNC2:20;
then f . x = - ((max- f) . x) ;
hence f . x = (- (max- f)) . x by b1, b2, MESFUNC1:def 7; :: thesis: verum
end;
hence f = - (max- f) by b1, PARTFUN1:5; :: thesis: verum