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

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