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 f is_a.e.integrable_on M holds
dom f in S
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL st f is_a.e.integrable_on M holds
dom f in S
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL st f is_a.e.integrable_on M holds
dom f in S
let f be PartFunc of X,ExtREAL; :: thesis: ( f is_a.e.integrable_on M implies dom f in S )
assume f is_a.e.integrable_on M ; :: thesis: dom f in S
then consider A being Element of S such that
A1: ( M . A = 0 & A c= dom f & f | (A `) is_integrable_on M ) ;
consider B being Element of S such that
A2: ( B = dom (f | (A `)) & f | (A `) is B -measurable ) by A1, MESFUNC5:def 17;
dom (f | (A `)) = (dom f) /\ (A `) by RELAT_1:61
.= (dom f) /\ (X \ A) by SUBSET_1:def 4
.= ((dom f) /\ X) \ A by XBOOLE_1:49
.= (dom f) \ A by XBOOLE_1:28 ;
then dom f = A \/ B by A1, A2, XBOOLE_1:45;
hence dom f in S ; :: thesis: verum