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 A3: 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 )
A5: for x being set st x in dom f holds
f . x = 0 by A2;
then A4: f is_simple_func_in S by A3, MESFUNC6:2;
A6: f is_measurable_on E by A3, A5, MESFUNC2:37, MESFUNC6:2;
A7: ( dom (max+ f) = dom f & ( for x being Element of X st x in dom (max+ f) holds
(max+ f) . x = max (f . x),0. ) ) by MESFUNC2:def 2;

A8: now

let x be Element of X; :: thesis: ( x in dom f implies f . x = (max+ f) . x )
assume A9: x in dom f ; :: thesis: f . x = (max+ f) . x
hence f . x = max 0 ,0 by A2
.= max (f . x),0 by A2, A9
.= (max+ f) . x by A7, A9 ;
:: thesis: verum

end;

A10: integral+ M,f = 0 by A3, A2, A4, MESFUNC2:37, MESFUNC5:93;
A11: f is nonnegative

proof

let y be R_eal; :: according to SUPINF_2:def 15,SUPINF_2:def 22 :: thesis: ( not y in rng f or 0. <= y )
assume y in rng f ; :: thesis: 0. <= y
then ex x1 being set st
( x1 in dom f & y = f . x1 ) by FUNCT_1:def 5;
hence y >= 0 by A2; :: thesis: verum

end;

then 0. = Integral M,f by A3, A4, A10, MESFUNC2:37, MESFUNC5:94
.= (integral+ M,f) - (integral+ M,(max- f)) by A7, A8, PARTFUN1:34
.= 0. + (- (integral+ M,(max- f))) by A3, A2, A4, MESFUNC2:37, MESFUNC5:93
.= - (integral+ M,(max- f)) by XXREAL_3:4 ;
then A14: - (- (integral+ M,(max- f))) = - 0 ;
integral+ M,(max+ f) < +infty by A7, A8, A10, PARTFUN1:34;
hence f is_integrable_on M by A3, A6, A14, MESFUNC5:def 17; :: thesis: Integral M,f = 0
thus Integral M,f = 0 by A3, A6, A10, A11, MESFUNC5:94; :: thesis: verum