let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f in L1_Functions M & g in L1_Functions M holds
f + g in L1_Functions M
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f in L1_Functions M & g in L1_Functions M holds
f + g in L1_Functions M
let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,REAL st f in L1_Functions M & g in L1_Functions M holds
f + g in L1_Functions M
let f, g be PartFunc of X,REAL; :: thesis: ( f in L1_Functions M & g in L1_Functions M implies f + g in L1_Functions M )
set W = L1_Functions M;
assume that
A1: f in L1_Functions M and
A2: g in L1_Functions M ; :: thesis: f + g in L1_Functions M
ex f1 being PartFunc of X,REAL st
( f1 = f & ex ND being Element of S st
( M . ND = 0 & dom f1 = ND ` & f1 is_integrable_on M ) ) by A1;
then consider NDv being Element of S such that
A3: M . NDv = 0 and
A4: dom f = NDv ` and
A5: f is_integrable_on M ;
ex g1 being PartFunc of X,REAL st
( g1 = g & ex ND being Element of S st
( M . ND = 0 & dom g1 = ND ` & g1 is_integrable_on M ) ) by A2;
then consider NDu being Element of S such that
A6: M . NDu = 0 and
A7: dom g = NDu ` and
A8: g is_integrable_on M ;
A9: dom (f + g) = (NDv `) /\ (NDu `) by A4, A7, VALUED_1:def 1
.= (NDv \/ NDu) ` by XBOOLE_1:53 ;
( M . (NDv \/ NDu) = 0 & f + g is_integrable_on M ) by A3, A5, A6, A8, Lm4, MESFUNC6:100;
hence f + g in L1_Functions M by A9; :: thesis: verum