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 f a.e.cpfunc= g,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 f a.e.cpfunc= g,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 f a.e.cpfunc= g,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 f a.e.cpfunc= g,M ) )
assume that
A1:
f in L1_CFunctions M
and
A2:
g in L1_CFunctions M
; ( a.e-Ceq-class (f,M) = a.e-Ceq-class (g,M) iff f a.e.cpfunc= g,M )
assume A3:
f a.e.cpfunc= g,M
; a.e-Ceq-class (f,M) = a.e-Ceq-class (g,M)
now for x being object st x in a.e-Ceq-class (f,M) holds
x in a.e-Ceq-class (g,M)let x be
object ;
( x in a.e-Ceq-class (f,M) implies x in a.e-Ceq-class (g,M) )assume
x in a.e-Ceq-class (
f,
M)
;
x in a.e-Ceq-class (g,M)then consider r being
PartFunc of
X,
COMPLEX such that A4:
(
x = r &
r in L1_CFunctions M )
and
f in L1_CFunctions M
and A5:
f a.e.cpfunc= r,
M
;
g a.e.cpfunc= f,
M
by A3;
then
g a.e.cpfunc= r,
M
by A5, Th24;
hence
x in a.e-Ceq-class (
g,
M)
by A2, A4;
verum end;
then A6:
a.e-Ceq-class (f,M) c= a.e-Ceq-class (g,M)
;
now for x being object st x in a.e-Ceq-class (g,M) holds
x in a.e-Ceq-class (f,M)let x be
object ;
( x in a.e-Ceq-class (g,M) implies x in a.e-Ceq-class (f,M) )assume
x in a.e-Ceq-class (
g,
M)
;
x in a.e-Ceq-class (f,M)then consider r being
PartFunc of
X,
COMPLEX such that A7:
(
x = r &
r in L1_CFunctions M )
and
g in L1_CFunctions M
and A8:
g a.e.cpfunc= r,
M
;
f a.e.cpfunc= r,
M
by A3, A8, Th24;
hence
x in a.e-Ceq-class (
f,
M)
by A1, A7;
verum end;
then
a.e-Ceq-class (g,M) c= a.e-Ceq-class (f,M)
;
hence
a.e-Ceq-class (f,M) = a.e-Ceq-class (g,M)
by A6, XBOOLE_0:def 10; verum