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 ex x being VECTOR of (Pre-L-CSpace M) st
( f in x & g in x ) holds
( f a.e.cpfunc= g,M & f in L1_CFunctions M & g in L1_CFunctions M )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,COMPLEX st ex x being VECTOR of (Pre-L-CSpace M) st
( f in x & g in x ) holds
( f a.e.cpfunc= g,M & f in L1_CFunctions M & g in L1_CFunctions M )
let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,COMPLEX st ex x being VECTOR of (Pre-L-CSpace M) st
( f in x & g in x ) holds
( f a.e.cpfunc= g,M & f in L1_CFunctions M & g in L1_CFunctions M )
let f, g be PartFunc of X,COMPLEX; :: thesis: ( ex x being VECTOR of (Pre-L-CSpace M) st
( f in x & g in x ) implies ( f a.e.cpfunc= g,M & f in L1_CFunctions M & g in L1_CFunctions M ) )
given x being VECTOR of (Pre-L-CSpace M) such that A1: f in x and
A2: g in x ; :: thesis: ( f a.e.cpfunc= g,M & f in L1_CFunctions M & g in L1_CFunctions M )
x in the carrier of (Pre-L-CSpace M) ;
then x in CCosetSet M by Def19;
then consider h being PartFunc of X,COMPLEX such that
A3: x = a.e-Ceq-class (h,M) and
h in L1_CFunctions M ;
ex k being PartFunc of X,COMPLEX st
( f = k & k in L1_CFunctions M & h in L1_CFunctions M & h a.e.cpfunc= k,M ) by A1, A3;
then A4: f a.e.cpfunc= h,M ;
ex j being PartFunc of X,COMPLEX st
( g = j & j in L1_CFunctions M & h in L1_CFunctions M & h a.e.cpfunc= j,M ) by A2, A3;
hence ( f a.e.cpfunc= g,M & f in L1_CFunctions M & g in L1_CFunctions M ) by A1, A3, A4, Th24; :: thesis: verum