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 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( ( 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 :: thesis: for x being Element of X st x in dom f holds
f . x = ((chi (0,E,X)) | E) . x

let x be Element of X; :: thesis: ( x in dom f implies f . x = ((chi (0,E,X)) | E) . x )
assume a4: x in dom f ; :: thesis: f . x = ((chi (0,E,X)) | E) . x
then ((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; :: thesis: 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; :: thesis: Integral (M,f) = 0
Integral (M,f) = 0 * (M . E) by a4, Th50;
hence Integral (M,f) = 0 ; :: thesis: verum