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

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

hence
f = - (max- f)
by b1, 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) = 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;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