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

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