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 st f in L1_Functions M & g in L1_Functions M holds
( a.e-eq-class (f,M) = a.e-eq-class (g,M) iff f a.e.= g,M )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f in L1_Functions M & g in L1_Functions M holds
( a.e-eq-class (f,M) = a.e-eq-class (g,M) iff f a.e.= g,M )
let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,REAL st f in L1_Functions M & g in L1_Functions M holds
( a.e-eq-class (f,M) = a.e-eq-class (g,M) iff f a.e.= g,M )
let f, g be PartFunc of X,REAL; :: thesis: ( f in L1_Functions M & g in L1_Functions M implies ( a.e-eq-class (f,M) = a.e-eq-class (g,M) iff f a.e.= g,M ) )
assume that
A1: f in L1_Functions M and
A2: g in L1_Functions M ; :: thesis: ( a.e-eq-class (f,M) = a.e-eq-class (g,M) iff f a.e.= g,M )

hereby :: thesis: ( f a.e.= g,M implies a.e-eq-class (f,M) = a.e-eq-class (g,M) )

assume a.e-eq-class (f,M) = a.e-eq-class (g,M) ; :: thesis: f a.e.= g,M
then f in { r where r is PartFunc of X,REAL : ( r in L1_Functions M & g in L1_Functions M & g a.e.= r,M ) } by A1, Th38;
then ex r being PartFunc of X,REAL st
( f = r & r in L1_Functions M & g in L1_Functions M & g a.e.= r,M ) ;
hence f a.e.= g,M ; :: thesis: verum

end;

assume A3: f a.e.= g,M ; :: thesis: a.e-eq-class (f,M) = a.e-eq-class (g,M)

now :: thesis: for x being object st x in a.e-eq-class (f,M) holds
x in a.e-eq-class (g,M)

let x be object ; :: thesis: ( x in a.e-eq-class (f,M) implies x in a.e-eq-class (g,M) )
assume x in a.e-eq-class (f,M) ; :: thesis: x in a.e-eq-class (g,M)
then consider r being PartFunc of X,REAL such that
A4: ( x = r & r in L1_Functions M ) and
f in L1_Functions M and
A5: f a.e.= r,M ;
g a.e.= f,M by A3;
then g a.e.= r,M by A5, Th30;
hence x in a.e-eq-class (g,M) by A2, A4; :: thesis: verum

end;

then A6: a.e-eq-class (f,M) c= a.e-eq-class (g,M) ;

now :: thesis: for x being object st x in a.e-eq-class (g,M) holds
x in a.e-eq-class (f,M)

let x be object ; :: thesis: ( x in a.e-eq-class (g,M) implies x in a.e-eq-class (f,M) )
assume x in a.e-eq-class (g,M) ; :: thesis: x in a.e-eq-class (f,M)
then consider r being PartFunc of X,REAL such that
A7: ( x = r & r in L1_Functions M ) and
g in L1_Functions M and
A8: g a.e.= r,M ;
f a.e.= r,M by A3, A8, Th30;
hence x in a.e-eq-class (f,M) by A1, A7; :: thesis: verum

end;

then a.e-eq-class (g,M) c= a.e-eq-class (f,M) ;
hence a.e-eq-class (f,M) = a.e-eq-class (g,M) by A6, XBOOLE_0:def 10; :: thesis: verum