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 g in a.e-eq-class f,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 g in a.e-eq-class f,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 g in a.e-eq-class f,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 g in a.e-eq-class f,M ) )
assume A1: ( f in L1_Functions M & g in L1_Functions M ) ; :: thesis: ( a.e-eq-class f,M = a.e-eq-class g,M iff g in a.e-eq-class f,M )
then ( g a.e.= f,M iff g in a.e-eq-class f,M ) by EQC00;
hence ( a.e-eq-class f,M = a.e-eq-class g,M iff g in a.e-eq-class f,M ) by A1, EQC02; :: thesis: verum