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

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