let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, f1, g, g1 being PartFunc of X,REAL st f a.e.= f1,M & g a.e.= g1,M holds
f + g a.e.= f1 + g1,M
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f, f1, g, g1 being PartFunc of X,REAL st f a.e.= f1,M & g a.e.= g1,M holds
f + g a.e.= f1 + g1,M
let M be sigma_Measure of S; :: thesis: for f, f1, g, g1 being PartFunc of X,REAL st f a.e.= f1,M & g a.e.= g1,M holds
f + g a.e.= f1 + g1,M
let f, f1, g, g1 be PartFunc of X,REAL ; :: thesis: ( f a.e.= f1,M & g a.e.= g1,M implies f + g a.e.= f1 + g1,M )
assume that
A1: f a.e.= f1,M and
A2: g a.e.= g1,M ; :: thesis: f + g a.e.= f1 + g1,M
consider EQ1 being Element of S such that
A3: ( M . EQ1 = 0 & f | (EQ1 ` ) = f1 | (EQ1 ` ) ) by A1, Def2;
consider EQ2 being Element of S such that
A4: ( M . EQ2 = 0 & g | (EQ2 ` ) = g1 | (EQ2 ` ) ) by A2, Def2;
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) ` ) = (f1 | (EQ1 ` )) | ((EQ1 \/ EQ2) ` ) by A3, FUNCT_1:82;
then A9: f | ((EQ1 \/ EQ2) ` ) = f1 | ((EQ1 \/ EQ2) ` ) by A8, FUNCT_1:82;
g | ((EQ1 \/ EQ2) ` ) = (g1 | (EQ2 ` )) | ((EQ1 \/ EQ2) ` ) by A4, A8, FUNCT_1:82
.= g1 | ((EQ1 \/ EQ2) ` ) by A8, FUNCT_1:82 ;
then (f + g) | ((EQ1 \/ EQ2) ` ) = (f1 | ((EQ1 \/ EQ2) ` )) + (g1 | ((EQ1 \/ EQ2) ` )) by A9, RFUNCT_1:60
.= (f1 + g1) | ((EQ1 \/ EQ2) ` ) by RFUNCT_1:60 ;
hence f + g a.e.= f1 + g1,M by Def2, A7; :: thesis: verum