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

.= 0 ;

:: thesis: integral+ (M,(max- f)) = 0

hence integral+ (M,(max- f)) = 0 by A3, A4, Th5, MESFUNC5:88; :: thesis: verum

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

hence Integral (M,(max- f)) =
0 * (M . (dom (max- f)))
by A3, MEASUR10:27
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;

end;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;

.= 0 ;

:: thesis: integral+ (M,(max- f)) = 0

hence integral+ (M,(max- f)) = 0 by A3, A4, Th5, MESFUNC5:88; :: thesis: verum