let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g, h being PartFunc of X,REAL st f a.e.= g,M & g a.e.= h,M holds
f a.e.= h,M
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f, g, h being PartFunc of X,REAL st f a.e.= g,M & g a.e.= h,M holds
f a.e.= h,M
let M be sigma_Measure of S; :: thesis: for f, g, h being PartFunc of X,REAL st f a.e.= g,M & g a.e.= h,M holds
f a.e.= h,M
let f, g, h be PartFunc of X,REAL ; :: thesis: ( f a.e.= g,M & g a.e.= h,M implies f a.e.= h,M )
assume that
A1: f a.e.= g,M and
A2: g a.e.= h,M ; :: thesis: f a.e.= h,M
consider EQ1 being Element of S such that
A3: ( M . EQ1 = 0 & f | (EQ1 ` ) = g | (EQ1 ` ) ) by Def2, A1;
consider EQ2 being Element of S such that
A4: ( M . EQ2 = 0 & g | (EQ2 ` ) = h | (EQ2 ` ) ) by Def2, A2;
A7: M . (EQ1 \/ EQ2) = 0 by A3, A4, MLm01;
A8: ( (EQ1 \/ EQ2) ` c= EQ1 ` & (EQ1 \/ EQ2) ` c= EQ2 ` ) by XBOOLE_1:7, XBOOLE_1:34;
then f | ((EQ1 \/ EQ2) ` ) = (g | (EQ1 ` )) | ((EQ1 \/ EQ2) ` ) by A3, FUNCT_1:82
.= g | ((EQ1 \/ EQ2) ` ) by A8, FUNCT_1:82
.= (h | (EQ2 ` )) | ((EQ1 \/ EQ2) ` ) by A4, A8, FUNCT_1:82
.= h | ((EQ1 \/ EQ2) ` ) by A8, FUNCT_1:82 ;
hence f a.e.= h,M by A7, Def2; :: thesis: verum