let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being nonnegative PartFunc of X,ExtREAL
for E being Element of S st E = dom f & f is E -measurable holds
( Integral (M,(max- f)) = 0 & integral+ (M,(max- f)) = 0 )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being nonnegative PartFunc of X,ExtREAL
for E being Element of S st E = dom f & f is E -measurable holds
( Integral (M,(max- f)) = 0 & integral+ (M,(max- f)) = 0 )
let M be sigma_Measure of S; :: thesis: for f being nonnegative PartFunc of X,ExtREAL
for E being Element of S st E = dom f & f is E -measurable holds
( Integral (M,(max- f)) = 0 & integral+ (M,(max- f)) = 0 )
let f be nonnegative PartFunc of X,ExtREAL; :: thesis: for E being Element of S st E = dom f & f is E -measurable holds
( Integral (M,(max- f)) = 0 & integral+ (M,(max- f)) = 0 )
let E be Element of S; :: thesis: ( E = dom f & f is E -measurable implies ( Integral (M,(max- f)) = 0 & integral+ (M,(max- f)) = 0 ) )
assume that
A1: E = dom f and
A2: f is E -measurable ; :: thesis: ( Integral (M,(max- f)) = 0 & integral+ (M,(max- f)) = 0 )
A3: E = dom (max- f) by A1, MESFUNC2:def 3;
A4: max- f is E -measurable by A1, A2, Th10;
for x being object st x in dom (max- f) holds
(max- f) . x = 0

proof

let x be object ; :: thesis: ( x in dom (max- f) implies (max- f) . x = 0 )
assume A5: x in dom (max- f) ; :: thesis: (max- f) . x = 0
then A6: x in dom (max+ f) by A1, A3, MESFUNC2:def 2;

per cases ( f . x = 0 or f . x > 0 ) by SUPINF_2:51;

suppose f . x = 0 ; :: thesis: (max- f) . x = 0

then (max+ f) . x = f . x by A5, MESFUNC2:18;
hence (max- f) . x = 0 by A5, MESFUNC2:19; :: thesis: verum

end;

suppose f . x > 0 ; :: thesis: (max- f) . x = 0

then max ((f . x),0) = f . x by XXREAL_0:def 10;
then (max+ f) . x = f . x by A6, MESFUNC2:def 2;
hence (max- f) . x = 0 by A5, MESFUNC2:19; :: thesis: verum

end;

end;

end;

hence Integral (M,(max- f)) = 0 * (M . (dom (max- f))) by A3, MEASUR10:27
.= 0 ;
:: thesis: integral+ (M,(max- f)) = 0
hence integral+ (M,(max- f)) = 0 by A3, A4, Th5, MESFUNC5:88; :: thesis: verum