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,REAL st f in L1_Functions M holds
( f is_integrable_on M & ex E being Element of S st
( M . (E `) = 0 & E = dom f & f is E -measurable ) )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,REAL st f in L1_Functions M holds
( f is_integrable_on M & ex E being Element of S st
( M . (E `) = 0 & E = dom f & f is E -measurable ) )
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,REAL st f in L1_Functions M holds
( f is_integrable_on M & ex E being Element of S st
( M . (E `) = 0 & E = dom f & f is E -measurable ) )
let f be PartFunc of X,REAL; :: thesis: ( f in L1_Functions M implies ( f is_integrable_on M & ex E being Element of S st
( M . (E `) = 0 & E = dom f & f is E -measurable ) ) )
assume f in L1_Functions M ; :: thesis: ( f is_integrable_on M & ex E being Element of S st
( M . (E `) = 0 & E = dom f & f is E -measurable ) )
then ex f2 being PartFunc of X,REAL st
( f = f2 & ex E being Element of S st
( M . E = 0 & dom f2 = E ` & f2 is_integrable_on M ) ) ;
then consider D being Element of S such that
A1: ( M . D = 0 & dom f = D ` & f is_integrable_on M ) ;
thus f is_integrable_on M by A1; :: thesis: ex E being Element of S st
( M . (E `) = 0 & E = dom f & f is E -measurable )
reconsider E = D ` as Element of S by MEASURE1:34;
take E ; :: thesis: ( M . (E `) = 0 & E = dom f & f is E -measurable )
thus ( M . (E `) = 0 & dom f = E ) by A1; :: thesis: f is E -measurable
R_EAL f is_integrable_on M by A1;
then ex B being Element of S st
( B = dom (R_EAL f) & R_EAL f is B -measurable ) ;
hence f is E -measurable by A1; :: thesis: verum