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 ) )
assume A1: ex E being Element of S st 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 )
consider E being Element of S such that
A3: E = dom f by A1;
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 A1, MESFUNC6:2;
A6: f is_measurable_on E by A1, 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 A1, 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 A13: 0. = Integral M,f by A1, A4, A10, MESFUNC2:37, MESFUNC5:94
.= (integral+ M,f) - (integral+ M,(max- f)) by A7, A8, PARTFUN1:34
.= 0. + (- (integral+ M,(max- f))) by A1, A2, A4, MESFUNC2:37, MESFUNC5:93
.= - (integral+ M,(max- f)) by SUPINF_2:18 ;
integral+ M,(max+ f) < +infty by A7, A8, A10, PARTFUN1:34;
hence ( f is_integrable_on M & Integral M,f = 0 ) by A3, A6, A10, A11, A13, EXTREAL1:24, MESFUNC5:94, MESFUNC5:def 17; :: thesis: verum