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 that
A1: f in L1_Functions M and
A2: g in L1_Functions M and
A3: f a.e.= g,M ; :: thesis: Integral (M,f) = Integral (M,g)
consider EQ being Element of S such that
A4: M . EQ = 0 and
A5: f | (EQ `) = g | (EQ `) by A3;
A6: 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
A7: M . NDf = 0 and
A8: dom f = NDf ` and
f is_integrable_on M ;
A9: M . (EQ \/ NDf) = 0 by A7, A4, Lm4;
R_EAL f is_integrable_on M by A6;
then consider E1 being Element of S such that
A10: E1 = dom (R_EAL f) and
A11: R_EAL f is E1 -measurable ;
A12: f is E1 -measurable by A11;
A13: 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 A2;
then consider NDg being Element of S such that
A14: M . NDg = 0 and
A15: dom g = NDg ` and
g is_integrable_on M ;
A16: M . (EQ \/ NDg) = 0 by A14, A4, Lm4;
R_EAL g is_integrable_on M by A13;
then consider E2 being Element of S such that
A17: E2 = dom (R_EAL g) and
A18: R_EAL g is E2 -measurable ;
A19: g is E2 -measurable by A18;
A20: (EQ `) \ (NDf \/ NDg) = (EQ \/ (NDf \/ NDg)) ` by XBOOLE_1:41
.= (NDg \/ (EQ \/ NDf)) ` by XBOOLE_1:4
.= (NDg `) \ (EQ \/ NDf) by XBOOLE_1:41 ;
A21: (EQ `) \ (NDf \/ NDg) = (EQ \/ (NDf \/ NDg)) ` by XBOOLE_1:41
.= (NDf \/ (EQ \/ NDg)) ` by XBOOLE_1:4
.= (NDf `) \ (EQ \/ NDg) by XBOOLE_1:41 ;
A22: (EQ `) \ (NDf \/ NDg) c= EQ ` by XBOOLE_1:36;
then f | ((EQ `) \ (NDf \/ NDg)) = (g | (EQ `)) | ((EQ `) \ (NDf \/ NDg)) by A5, FUNCT_1:51
.= g | ((EQ `) \ (NDf \/ NDg)) by A22, FUNCT_1:51 ;
hence Integral (M,f) = Integral (M,(g | ((NDg `) \ (EQ \/ NDf)))) by A8, A10, A12, A21, A20, A16, MESFUNC6:89
.= Integral (M,g) by A15, A17, A19, A9, MESFUNC6:89 ;
:: thesis: verum