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