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

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

assume g a.e.cpfunc= f,M ; :: thesis: g in a.e-Ceq-class (f,M)
then f a.e.cpfunc= g,M ;
hence g in a.e-Ceq-class (f,M) by A1; :: thesis: verum

end;

assume g in a.e-Ceq-class (f,M) ; :: thesis: g a.e.cpfunc= f,M
then ex r being PartFunc of X,COMPLEX st
( g = r & r in L1_CFunctions M & f in L1_CFunctions M & f a.e.cpfunc= r,M ) ;
hence g a.e.cpfunc= f,M ; :: thesis: verum