let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL
for k being positive Real st f a.e.= g,M holds
a.e-eq-class_Lp f,M,k = a.e-eq-class_Lp g,M,k
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,REAL
for k being positive Real st f a.e.= g,M holds
a.e-eq-class_Lp f,M,k = a.e-eq-class_Lp g,M,k
let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,REAL
for k being positive Real st f a.e.= g,M holds
a.e-eq-class_Lp f,M,k = a.e-eq-class_Lp g,M,k
let f, g be PartFunc of X,REAL ; :: thesis: for k being positive Real st f a.e.= g,M holds
a.e-eq-class_Lp f,M,k = a.e-eq-class_Lp g,M,k
let k be positive Real; :: thesis: ( f a.e.= g,M implies a.e-eq-class_Lp f,M,k = a.e-eq-class_Lp g,M,k )
assume A2: f a.e.= g,M ; :: thesis: a.e-eq-class_Lp f,M,k = a.e-eq-class_Lp g,M,k

now

let x be set ; :: thesis: ( x in a.e-eq-class_Lp f,M,k implies x in a.e-eq-class_Lp g,M,k )
assume x in a.e-eq-class_Lp f,M,k ; :: thesis: x in a.e-eq-class_Lp g,M,k
then consider r being PartFunc of X,REAL such that
A3: ( x = r & r in Lp_Functions M,k & f a.e.= r,M ) ;
r a.e.= f,M by A3, LPSPACE1:29;
then r a.e.= g,M by A2, LPSPACE1:30;
then g a.e.= r,M by LPSPACE1:29;
hence x in a.e-eq-class_Lp g,M,k by A3; :: thesis: verum

end;

then A4: a.e-eq-class_Lp f,M,k c= a.e-eq-class_Lp g,M,k by TARSKI:def 3;

now

let x be set ; :: thesis: ( x in a.e-eq-class_Lp g,M,k implies x in a.e-eq-class_Lp f,M,k )
assume x in a.e-eq-class_Lp g,M,k ; :: thesis: x in a.e-eq-class_Lp f,M,k
then consider r being PartFunc of X,REAL such that
A5: ( x = r & r in Lp_Functions M,k & g a.e.= r,M ) ;
( r a.e.= g,M & g a.e.= f,M ) by A2, A5, LPSPACE1:29;
then r a.e.= f,M by LPSPACE1:30;
then f a.e.= r,M by LPSPACE1:29;
hence x in a.e-eq-class_Lp f,M,k by A5; :: thesis: verum

end;

then a.e-eq-class_Lp g,M,k c= a.e-eq-class_Lp f,M,k by TARSKI:def 3;
hence a.e-eq-class_Lp f,M,k = a.e-eq-class_Lp g,M,k by A4, XBOOLE_0:def 10; :: thesis: verum