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 ex x being VECTOR of (Pre-L-Space M) st
( f in x & g in x ) holds
( f a.e.= g,M & f in L1_Functions M & g in L1_Functions M )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st ex x being VECTOR of (Pre-L-Space M) st
( f in x & g in x ) holds
( f a.e.= g,M & f in L1_Functions M & g in L1_Functions M )
let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,REAL st ex x being VECTOR of (Pre-L-Space M) st
( f in x & g in x ) holds
( f a.e.= g,M & f in L1_Functions M & g in L1_Functions M )
let f, g be PartFunc of X,REAL; :: thesis: ( ex x being VECTOR of (Pre-L-Space M) st
( f in x & g in x ) implies ( f a.e.= g,M & f in L1_Functions M & g in L1_Functions M ) )
assume ex x being VECTOR of (Pre-L-Space M) st
( f in x & g in x ) ; :: thesis: ( f a.e.= g,M & f in L1_Functions M & g in L1_Functions M )
then consider x being VECTOR of (Pre-L-Space M) such that
A1: f in x and
A2: g in x ;
x in the carrier of (Pre-L-Space M) ;
then x in CosetSet M by Def18;
then consider h being PartFunc of X,REAL such that
A3: x = a.e-eq-class (h,M) and
h in L1_Functions M ;
ex k being PartFunc of X,REAL st
( f = k & k in L1_Functions M & h in L1_Functions M & h a.e.= k,M ) by A1, A3;
then A4: f a.e.= h,M ;
ex j being PartFunc of X,REAL st
( g = j & j in L1_Functions M & h in L1_Functions M & h a.e.= j,M ) by A2, A3;
hence ( f a.e.= g,M & f in L1_Functions M & g in L1_Functions M ) by A1, A3, A4, Th30; :: thesis: verum