let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g, f1, 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, g, f1, 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, g, f1, 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, g, f1, 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 and
A4: f | (EQ1 `) = f1 | (EQ1 `) by A1;
consider EQ2 being Element of S such that
A5: M . EQ2 = 0 and
A6: g | (EQ2 `) = g1 | (EQ2 `) by A2;
A7: (EQ1 \/ EQ2) ` c= EQ1 ` by XBOOLE_1:7, XBOOLE_1:34;
then f | ((EQ1 \/ EQ2) `) = (f1 | (EQ1 `)) | ((EQ1 \/ EQ2) `) by A4, FUNCT_1:51;
then A8: f | ((EQ1 \/ EQ2) `) = f1 | ((EQ1 \/ EQ2) `) by A7, FUNCT_1:51;
A9: (EQ1 \/ EQ2) ` c= EQ2 ` by XBOOLE_1:7, XBOOLE_1:34;
then g | ((EQ1 \/ EQ2) `) = (g1 | (EQ2 `)) | ((EQ1 \/ EQ2) `) by A6, FUNCT_1:51
.= g1 | ((EQ1 \/ EQ2) `) by A9, FUNCT_1:51 ;
then A10: (f + g) | ((EQ1 \/ EQ2) `) = (f1 | ((EQ1 \/ EQ2) `)) + (g1 | ((EQ1 \/ EQ2) `)) by A8, RFUNCT_1:44
.= (f1 + g1) | ((EQ1 \/ EQ2) `) by RFUNCT_1:44 ;
M . (EQ1 \/ EQ2) = 0 by A3, A5, Lm4;
hence f + g a.e.= f1 + g1,M by A10; :: thesis: verum