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 dom f in S & ( for x being Element of X st x in dom f holds
0 = f . x ) holds
( ( for E being Element of S st E c= dom f holds
f is E -measurable ) & 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 dom f in S & ( for x being Element of X st x in dom f holds
0 = f . x ) holds
( ( for E being Element of S st E c= dom f holds
f is E -measurable ) & Integral (M,f) = 0 )
let M be sigma_Measure of S; for f being PartFunc of X,ExtREAL st dom f in S & ( for x being Element of X st x in dom f holds
0 = f . x ) holds
( ( for E being Element of S st E c= dom f holds
f is E -measurable ) & Integral (M,f) = 0 )
let f be PartFunc of X,ExtREAL; ( dom f in S & ( for x being Element of X st x in dom f holds
0 = f . x ) implies ( ( for E being Element of S st E c= dom f holds
f is E -measurable ) & Integral (M,f) = 0 ) )
assume that
a1:
dom f in S
and
a2:
for x being Element of X st x in dom f holds
f . x = 0
; ( ( for E being Element of S st E c= dom f holds
f is E -measurable ) & Integral (M,f) = 0 )
reconsider E = dom f as Element of S by a1;
dom ((chi (0,E,X)) | E) = (dom (chi (0,E,X))) /\ E
by RELAT_1:61;
then
dom ((chi (0,E,X)) | E) = X /\ E
by FUNCT_2:def 1;
then a3:
dom ((chi (0,E,X)) | E) = E
by XBOOLE_1:28;
now for x being Element of X st x in dom f holds
f . x = ((chi (0,E,X)) | E) . xlet x be
Element of
X;
( x in dom f implies f . x = ((chi (0,E,X)) | E) . x )assume a4:
x in dom f
;
f . x = ((chi (0,E,X)) | E) . xthen
((chi (0,E,X)) | E) . x = (chi (0,E,X)) . x
by FUNCT_1:49;
then
((chi (0,E,X)) | E) . x = 0
by a4, Def1;
hence
f . x = ((chi (0,E,X)) | E) . x
by a2, a4;
verum end;
then a4:
f = (chi (0,E,X)) | E
by a3, PARTFUN1:5;
hence
for A being Element of S st A c= dom f holds
f is A -measurable
by Th15; Integral (M,f) = 0
Integral (M,f) = 0 * (M . E)
by a4, Th50;
hence
Integral (M,f) = 0
; verum