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,COMPLEX
for x being Point of (Pre-L-CSpace M) st f in x holds
( f is_integrable_on M & f in L1_CFunctions M & abs f is_integrable_on M )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX
for x being Point of (Pre-L-CSpace M) st f in x holds
( f is_integrable_on M & f in L1_CFunctions M & abs f is_integrable_on M )
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,COMPLEX
for x being Point of (Pre-L-CSpace M) st f in x holds
( f is_integrable_on M & f in L1_CFunctions M & abs f is_integrable_on M )
let f be PartFunc of X,COMPLEX; :: thesis: for x being Point of (Pre-L-CSpace M) st f in x holds
( f is_integrable_on M & f in L1_CFunctions M & abs f is_integrable_on M )
let x be Point of (Pre-L-CSpace M); :: thesis: ( f in x implies ( f is_integrable_on M & f in L1_CFunctions M & abs f is_integrable_on M ) )
x in the carrier of (Pre-L-CSpace M) ;
then x in CCosetSet M by Def19;
then consider h being PartFunc of X,COMPLEX such that
A1: x = a.e-Ceq-class (h,M) and
h in L1_CFunctions M ;
assume f in x ; :: thesis: ( f is_integrable_on M & f in L1_CFunctions M & abs f is_integrable_on M )
then ex g being PartFunc of X,COMPLEX st
( f = g & g in L1_CFunctions M & h in L1_CFunctions M & h a.e.cpfunc= g,M ) by A1;
then ex f0 being PartFunc of X,COMPLEX st
( f = f0 & ex ND being Element of S st
( M . ND = 0 & dom f0 = ND ` & f0 is_integrable_on M ) ) ;
hence ( f is_integrable_on M & f in L1_CFunctions M & abs f is_integrable_on M ) by Th37; :: thesis: verum