let X be non empty set ; 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; 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; 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; ( 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
; 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; verum