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 f a.e.= g,M holds
f a.e.= g, COM M
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f a.e.= g,M holds
f a.e.= g, COM M
let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,REAL st f a.e.= g,M holds
f a.e.= g, COM M
let f, g be PartFunc of X,REAL; :: thesis: ( f a.e.= g,M implies f a.e.= g, COM M )
assume f a.e.= g,M ; :: thesis: f a.e.= g, COM M
then consider E being Element of S such that
A1: ( M . E = 0 & f | (E `) = g | (E `) ) by LPSPACE1:def 10;
reconsider E0 = {} as Element of S by MEASURE1:7;
M . E0 = 0 by VALUED_0:def 19;
then A2: E0 is thin of M by MEASURE3:def 2;
A3: E = E \/ E0 ;
reconsider E1 = E as Element of COM (S,M) by Th27;
(COM M) . E1 = 0 by A1, A2, A3, MEASURE3:def 5;
hence f a.e.= g, COM M by A1, LPSPACE1:def 10; :: thesis: verum