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 A being Element of S st
( A = dom f & f is A -measurable ) & ( for x being Element of X st x in dom f holds
0 = f . x ) holds
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 A being Element of S st
( A = dom f & f is A -measurable ) & ( for x being Element of X st x in dom f holds
0 = f . x ) holds
integral+ (M,f) = 0
let M be sigma_Measure of S; for f being PartFunc of X,ExtREAL st ex A being Element of S st
( A = dom f & f is A -measurable ) & ( for x being Element of X st x in dom f holds
0 = f . x ) holds
integral+ (M,f) = 0
let f be PartFunc of X,ExtREAL; ( ex A being Element of S st
( A = dom f & f is A -measurable ) & ( for x being Element of X st x in dom f holds
0 = f . x ) implies integral+ (M,f) = 0 )
assume that
A1:
ex A being Element of S st
( A = dom f & f is A -measurable )
and
A2:
for x being Element of X st x in dom f holds
0 = f . x
; integral+ (M,f) = 0
A3:
for x being object st x in dom f holds
0 <= f . x
by A2;
A4:
dom (0 (#) f) = dom f
by MESFUNC1:def 6;
hence integral+ (M,f) =
integral+ (M,(0 (#) f))
by A4, FUNCT_1:2
.=
0 * (integral+ (M,f))
by A1, A3, Th86, SUPINF_2:52
.=
0
;
verum