let X be non empty set ; 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; 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; 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; ( 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
; ( 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
; ( 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;
A9:
f is E -measurable
by A1, A3, MESFUNC2:34, MESFUNC6:2;
A10:
f is nonnegative
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; Integral (M,f) = 0
thus
Integral (M,f) = 0
by A1, A9, A5, A10, MESFUNC5:88; verum