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

now

let x be set ; :: thesis: ( x in a.e-eq-class f,M implies 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 by MESFUNC6:def 9;
then consider A being Element of S such that
A5: ( A = dom (R_EAL g) & R_EAL g is_measurable_on A ) by MESFUNC5:def 17;
A6: ( A = dom g & g is_measurable_on A ) by A5, MESFUNC6:def 6;
A7: M . (A ` ) = 0 by A2, A5;
(abs g) to_power 1 = abs g by LmPW006;
then (abs g) to_power 1 is_integrable_on M by A2, A6, 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_measurable_on Ep & (abs p) to_power 1 is_integrable_on M ) } by A6, A7;
hence x in a.e-eq-class_Lp f,M,1 by A1; :: thesis: verum

end;

hence a.e-eq-class f,M c= a.e-eq-class_Lp f,M,1 by TARSKI:def 3; :: thesis: verum