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 and
A4: f | (EQ1 `) = g | (EQ1 `) by A1;
consider EQ2 being Element of S such that
A5: M . EQ2 = 0 and
A6: g | (EQ2 `) = h | (EQ2 `) by A2;
A7: M . (EQ1 \/ EQ2) = 0 by A3, A5, Lm4;
A8: (EQ1 \/ EQ2) ` c= EQ2 ` by XBOOLE_1:7, XBOOLE_1:34;
A9: (EQ1 \/ EQ2) ` c= EQ1 ` by XBOOLE_1:7, XBOOLE_1:34;
then f | ((EQ1 \/ EQ2) `) = (g | (EQ1 `)) | ((EQ1 \/ EQ2) `) by A4, FUNCT_1:51
.= g | ((EQ1 \/ EQ2) `) by A9, FUNCT_1:51
.= (h | (EQ2 `)) | ((EQ1 \/ EQ2) `) by A6, A8, FUNCT_1:51
.= h | ((EQ1 \/ EQ2) `) by A8, FUNCT_1:51 ;
hence f a.e.= h,M by A7; :: thesis: verum