theorem :: LPSPACE1:40
for X being non empty set
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 g in a.e-eq-class (f,M) )