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 & f a.e.= g,M holds
Integral M,f = Integral M,g
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 & f a.e.= g,M holds
Integral M,f = Integral M,g
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 & f a.e.= g,M holds
Integral M,f = Integral M,g
let f, g be PartFunc of X,REAL ; :: thesis: ( f in L1_Functions M & g in L1_Functions M & f a.e.= g,M implies Integral M,f = Integral M,g )
assume A1: ( f in L1_Functions M & g in L1_Functions M & f a.e.= g,M ) ; :: thesis: Integral M,f = Integral M,g
A2: ex f1 being PartFunc of X,REAL st
( f = f1 & ex ND being Element of S st
( M . ND = 0 & dom f1 = ND ` & f1 is_integrable_on M ) ) by A1;
then consider NDf being Element of S such that
A3: ( M . NDf = 0 & dom f = NDf ` & f is_integrable_on M ) ;
A4: ex g1 being PartFunc of X,REAL st
( g = g1 & ex ND being Element of S st
( M . ND = 0 & dom g1 = ND ` & g1 is_integrable_on M ) ) by A1;
then consider NDg being Element of S such that
A5: ( M . NDg = 0 & dom g = NDg ` & g is_integrable_on M ) ;
consider EQ being Element of S such that
A6: ( M . EQ = 0 & f | (EQ ` ) = g | (EQ ` ) ) by A1, Def2;
R_EAL f is_integrable_on M by A2, MESFUNC6:def 9;
then consider E1 being Element of S such that
A7: ( E1 = dom (R_EAL f) & R_EAL f is_measurable_on E1 ) by MESFUNC5:def 17;
A8: ( E1 = dom f & f is_measurable_on E1 ) by A7, MESFUNC6:def 6;
R_EAL g is_integrable_on M by A4, MESFUNC6:def 9;
then consider E2 being Element of S such that
A9: ( E2 = dom (R_EAL g) & R_EAL g is_measurable_on E2 ) by MESFUNC5:def 17;
A10: ( E2 = dom g & g is_measurable_on E2 ) by A9, MESFUNC6:def 6;
A11: (EQ ` ) \ (NDf \/ NDg) = (EQ \/ (NDf \/ NDg)) ` by XBOOLE_1:41
.= (NDf \/ (EQ \/ NDg)) ` by XBOOLE_1:4
.= (NDf ` ) \ (EQ \/ NDg) by XBOOLE_1:41 ;
A12: (EQ ` ) \ (NDf \/ NDg) = (EQ \/ (NDf \/ NDg)) ` by XBOOLE_1:41
.= (NDg \/ (EQ \/ NDf)) ` by XBOOLE_1:4
.= (NDg ` ) \ (EQ \/ NDf) by XBOOLE_1:41 ;
A13: (EQ ` ) \ (NDf \/ NDg) c= EQ ` by XBOOLE_1:36;
then A14: f | ((EQ ` ) \ (NDf \/ NDg)) = (g | (EQ ` )) | ((EQ ` ) \ (NDf \/ NDg)) by A6, FUNCT_1:82
.= g | ((EQ ` ) \ (NDf \/ NDg)) by A13, FUNCT_1:82 ;
A17: M . (EQ \/ NDf) = 0 by A3, A6, MLm01;
M . (EQ \/ NDg) = 0 by A5, A6, MLm01;
hence Integral M,f = Integral M,(g | ((NDg ` ) \ (EQ \/ NDf))) by A3, A8, A11, A12, A14, MESFUNC6:89
.= Integral M,g by A5, A10, A17, MESFUNC6:89 ;
:: thesis: verum