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
for E being Element of S st M is complete & f is_integrable_on M & f a.e.= g,M & E = dom f & E = dom g holds
( g is_integrable_on M & 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
for E being Element of S st M is complete & f is_integrable_on M & f a.e.= g,M & E = dom f & E = dom g holds
( g is_integrable_on M & Integral (M,f) = Integral (M,g) )

let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,REAL
for E being Element of S st M is complete & f is_integrable_on M & f a.e.= g,M & E = dom f & E = dom g holds
( g is_integrable_on M & Integral (M,f) = Integral (M,g) )

let f, g be PartFunc of X,REAL; :: thesis: for E being Element of S st M is complete & f is_integrable_on M & f a.e.= g,M & E = dom f & E = dom g holds
( g is_integrable_on M & Integral (M,f) = Integral (M,g) )

let E be Element of S; :: thesis: ( M is complete & f is_integrable_on M & f a.e.= g,M & E = dom f & E = dom g implies ( g is_integrable_on M & Integral (M,f) = Integral (M,g) ) )
assume that
A1: M is complete and
A2: f is_integrable_on M and
A3: f a.e.= g,M and
A4: E = dom f and
A5: E = dom g ; :: thesis: ( g is_integrable_on M & Integral (M,f) = Integral (M,g) )
A6: R_EAL f is_integrable_on M by ;
then consider E1 being Element of S such that
A7: ( E1 = dom () & R_EAL f is E1 -measurable ) by MESFUNC5:def 17;
A8: integral+ (M,(max+ ())) < +infty by ;
A9: integral+ (M,(max- ())) < +infty by ;
A10: ( R_EAL f = f & R_EAL g = g ) by MESFUNC5:def 7;
then A11: f is E -measurable by ;
then A12: R_EAL g is E -measurable by ;
A13: ( E = dom (max+ f) & E = dom (max+ g) ) by ;
( max+ () is E -measurable & max+ () is E -measurable ) by ;
then A14: ( R_EAL (max+ f) is E -measurable & R_EAL (max+ g) is E -measurable ) by Th43;
then A15: ( max+ f is E -measurable & max+ g is E -measurable ) by MESFUNC6:def 1;
then Integral (M,(max+ f)) = integral+ (M,(R_EAL (max+ f))) by ;
then A16: Integral (M,(max+ f)) < +infty by ;
consider E0 being Element of S such that
A17: ( M . E0 = 0 & f | (E0 `) = g | (E0 `) ) by ;
consider E2 being Element of S such that
A18: ( M . E2 = 0 & (max+ f) | (E2 `) = (max+ g) | (E2 `) ) by ;
(max+ f) | (X \ E2) = (max+ f) | (E2 `) by SUBSET_1:def 4;
then (max+ f) | (X \ E2) = (max+ g) | (X \ E2) by ;
then (max+ f) | (E \ E2) = ((max+ g) | (X \ E2)) | (E \ E2) by ;
then A19: (max+ f) | (E \ E2) = (max+ g) | (E \ E2) by ;
Integral (M,(max+ f)) = Integral (M,((max+ f) | (E \ E2))) by ;
then Integral (M,(max+ f)) = Integral (M,(max+ g)) by ;
then integral+ (M,(R_EAL (max+ g))) < +infty by ;
then A20: integral+ (M,(max+ ())) < +infty by Th43;
A21: ( E = dom (max- f) & E = dom (max- g) ) by ;
( max- () is E -measurable & max- () is E -measurable ) by ;
then A22: ( R_EAL (max- f) is E -measurable & R_EAL (max- g) is E -measurable ) by Th43;
then A23: ( max- f is E -measurable & max- g is E -measurable ) by MESFUNC6:def 1;
then Integral (M,(max- f)) = integral+ (M,(R_EAL (max- f))) by ;
then A24: Integral (M,(max- f)) < +infty by ;
consider E3 being Element of S such that
A25: ( M . E3 = 0 & (max- f) | (E3 `) = (max- g) | (E3 `) ) by ;
(max- f) | (X \ E3) = (max- f) | (E3 `) by SUBSET_1:def 4;
then (max- f) | (X \ E3) = (max- g) | (X \ E3) by ;
then (max- f) | (E \ E3) = ((max- g) | (X \ E3)) | (E \ E3) by ;
then A26: (max- f) | (E \ E3) = (max- g) | (E \ E3) by ;
Integral (M,(max- f)) = Integral (M,((max- f) | (E \ E3))) by ;
then Integral (M,(max- f)) = Integral (M,(max- g)) by ;
then integral+ (M,(R_EAL (max- g))) < +infty by ;
then integral+ (M,(max- ())) < +infty by Th43;
hence g is_integrable_on M by ; :: thesis: Integral (M,f) = Integral (M,g)
f | (E \ E0) = (f | (X \ E0)) | (E \ E0) by ;
then f | (E \ E0) = (f | (E0 `)) | (E \ E0) by SUBSET_1:def 4;
then f | (E \ E0) = (g | (X \ E0)) | (E \ E0) by ;
then A27: f | (E \ E0) = g | (E \ E0) by ;
Integral (M,f) = Integral (M,(f | (E \ E0))) by ;
hence Integral (M,f) = Integral (M,g) by A5, A17, A27, A11, A1, A3, A4, Th26, MESFUNC6:89; :: thesis: verum