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 holds a.e-eq-class (f,M) c= a.e-eq-class_Lp (f,M,1)
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,REAL holds a.e-eq-class (f,M) c= a.e-eq-class_Lp (f,M,1)
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,REAL holds a.e-eq-class (f,M) c= a.e-eq-class_Lp (f,M,1)
let f be PartFunc of X,REAL; :: thesis: a.e-eq-class (f,M) c= a.e-eq-class_Lp (f,M,1)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in a.e-eq-class (f,M) or x in a.e-eq-class_Lp (f,M,1) )
assume x in a.e-eq-class (f,M) ; :: thesis: x in a.e-eq-class_Lp (f,M,1)
then consider g being PartFunc of X,REAL such that
A1: ( x = g & g in L1_Functions M & f in L1_Functions M & f a.e.= g,M ) ;
A2: ex h being PartFunc of X,REAL st
( g = h & ex D being Element of S st
( M . D = 0 & dom h = D ` & h is_integrable_on M ) ) by A1;
then R_EAL g is_integrable_on M ;
then consider A being Element of S such that
A3: ( A = dom (R_EAL g) & R_EAL g is A -measurable ) ;
A4: ( A = dom g & g is A -measurable ) by A3;
A5: M . (A `) = 0 by A2, A3;
(abs g) to_power 1 = abs g by Th8;
then (abs g) to_power 1 is_integrable_on M by A2, A4, MESFUNC6:94;
then g in { p where p is PartFunc of X,REAL : ex Ep being Element of S st
( M . (Ep `) = 0 & dom p = Ep & p is Ep -measurable & (abs p) to_power 1 is_integrable_on M ) } by A4, A5;
hence x in a.e-eq-class_Lp (f,M,1) by A1; :: thesis: verum