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