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 A1: ( f in L1_Functions M & g in L1_Functions M ) ; :: thesis: f + g in L1_Functions M
then 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 ) ) ;
then consider NDv being Element of S such that
A3: ( M . NDv = 0 & dom f = NDv ` & 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 A1;
then consider NDu being Element of S such that
A5: ( M . NDu = 0 & dom g = NDu ` & g is_integrable_on M ) ;
A6: ( M . (NDv \/ NDu) = 0 & f + g is_integrable_on M ) by A3, A5, MLm01, MESFUNC6:100;
dom (f + g) = (NDv ` ) /\ (NDu ` ) by A5, A3, VALUED_1:def 1
.= (NDv \/ NDu) ` by XBOOLE_1:53 ;
hence f + g in L1_Functions M by A6; :: thesis: verum