let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL st ex E being Element of S st E = dom f & ( for x being Element of X st x in dom f holds
0 = f . x ) holds
( f is_integrable_on M & Integral (M,f) = 0 )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL st ex E being Element of S st E = dom f & ( for x being Element of X st x in dom f holds
0 = f . x ) holds
( f is_integrable_on M & Integral (M,f) = 0 )
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL st ex E being Element of S st E = dom f & ( for x being Element of X st x in dom f holds
0 = f . x ) holds
( f is_integrable_on M & Integral (M,f) = 0 )
let f be PartFunc of X,ExtREAL; :: thesis: ( ex E being Element of S st E = dom f & ( for x being Element of X st x in dom f holds
0 = f . x ) implies ( f is_integrable_on M & Integral (M,f) = 0 ) )
given E being Element of S such that A1: E = dom f ; :: thesis: ( ex x being Element of X st
( x in dom f & not 0 = f . x ) or ( f is_integrable_on M & Integral (M,f) = 0 ) )
assume A2: for x being Element of X st x in dom f holds
0 = f . x ; :: thesis: ( f is_integrable_on M & Integral (M,f) = 0 )
then A3: for x being object st x in dom f holds
f . x = 0 ;
then A4: f is_simple_func_in S by A1, MESFUNC6:2;
then A5: integral+ (M,f) = 0 by A1, A2, MESFUNC2:34, MESFUNC5:87;
A6: dom (max+ f) = dom f by MESFUNC2:def 2;

A7: now :: thesis: for x being Element of X st x in dom f holds
f . x = (max+ f) . x

let x be Element of X; :: thesis: ( x in dom f implies f . x = (max+ f) . x )
assume A8: x in dom f ; :: thesis: f . x = (max+ f) . x
hence f . x = max (0,0) by A2
.= max ((f . x),0) by A2, A8
.= (max+ f) . x by A6, A8, MESFUNC2:def 2 ;
:: thesis: verum

end;

A9: f is E -measurable by A1, A3, MESFUNC2:34, MESFUNC6:2;
A10: f is nonnegative

proof

let y be ExtReal; :: according to SUPINF_2:def 9,SUPINF_2:def 11 :: thesis: ( not y in rng f or 0. <= y )
assume y in rng f ; :: thesis: 0. <= y
then ex x1 being object st
( x1 in dom f & y = f . x1 ) by FUNCT_1:def 3;
hence y >= 0 by A2; :: thesis: verum

end;

then 0. = Integral (M,f) by A1, A4, A5, MESFUNC2:34, MESFUNC5:88
.= (integral+ (M,f)) - (integral+ (M,(max- f))) by A6, A7, PARTFUN1:5
.= 0. + (- (integral+ (M,(max- f)))) by A1, A2, A4, MESFUNC2:34, MESFUNC5:87
.= - (integral+ (M,(max- f))) by XXREAL_3:4 ;
then A11: - (- (integral+ (M,(max- f)))) = - 0 ;
integral+ (M,(max+ f)) < +infty by A6, A7, A5, PARTFUN1:5;
hence f is_integrable_on M by A1, A9, A11; :: thesis: Integral (M,f) = 0
thus Integral (M,f) = 0 by A1, A9, A5, A10, MESFUNC5:88; :: thesis: verum