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 A2, MESFUNC6:def 4;

then consider E1 being Element of S such that

A7: ( E1 = dom (R_EAL f) & R_EAL f is E1 -measurable ) by MESFUNC5:def 17;

A8: integral+ (M,(max+ (R_EAL f))) < +infty by A6, MESFUNC5:def 17;

A9: integral+ (M,(max- (R_EAL f))) < +infty by A6, MESFUNC5:def 17;

A10: ( R_EAL f = f & R_EAL g = g ) by MESFUNC5:def 7;

then A11: f is E -measurable by A4, A7, MESFUNC6:def 1;

then A12: R_EAL g is E -measurable by A1, A3, A4, Th26, MESFUNC6:def 1;

A13: ( E = dom (max+ f) & E = dom (max+ g) ) by A4, A5, RFUNCT_3:def 10;

( max+ (R_EAL f) is E -measurable & max+ (R_EAL g) is E -measurable ) by A4, A7, A12, A10, A5, MESFUN11:10;

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 A13, MESFUNC6:61, MESFUNC6:82;

then A16: Integral (M,(max+ f)) < +infty by A8, Th43;

consider E0 being Element of S such that

A17: ( M . E0 = 0 & f | (E0 `) = g | (E0 `) ) by A3, LPSPACE1:def 10;

consider E2 being Element of S such that

A18: ( M . E2 = 0 & (max+ f) | (E2 `) = (max+ g) | (E2 `) ) by A3, Th42, LPSPACE1:def 10;

(max+ f) | (X \ E2) = (max+ f) | (E2 `) by SUBSET_1:def 4;

then (max+ f) | (X \ E2) = (max+ g) | (X \ E2) by A18, SUBSET_1:def 4;

then (max+ f) | (E \ E2) = ((max+ g) | (X \ E2)) | (E \ E2) by XBOOLE_1:33, RELAT_1:74;

then A19: (max+ f) | (E \ E2) = (max+ g) | (E \ E2) by XBOOLE_1:33, RELAT_1:74;

Integral (M,(max+ f)) = Integral (M,((max+ f) | (E \ E2))) by A13, A14, A18, MESFUNC6:def 1, MESFUNC6:89;

then Integral (M,(max+ f)) = Integral (M,(max+ g)) by A13, A14, A18, A19, MESFUNC6:def 1, MESFUNC6:89;

then integral+ (M,(R_EAL (max+ g))) < +infty by A13, A15, A16, MESFUNC6:61, MESFUNC6:82;

then A20: integral+ (M,(max+ (R_EAL g))) < +infty by Th43;

A21: ( E = dom (max- f) & E = dom (max- g) ) by A4, A5, RFUNCT_3:def 11;

( max- (R_EAL f) is E -measurable & max- (R_EAL g) is E -measurable ) by A4, A7, A12, A10, A5, MESFUN11:10;

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 A21, MESFUNC6:61, MESFUNC6:82;

then A24: Integral (M,(max- f)) < +infty by A9, Th43;

consider E3 being Element of S such that

A25: ( M . E3 = 0 & (max- f) | (E3 `) = (max- g) | (E3 `) ) by A3, Th42, LPSPACE1:def 10;

(max- f) | (X \ E3) = (max- f) | (E3 `) by SUBSET_1:def 4;

then (max- f) | (X \ E3) = (max- g) | (X \ E3) by A25, SUBSET_1:def 4;

then (max- f) | (E \ E3) = ((max- g) | (X \ E3)) | (E \ E3) by XBOOLE_1:33, RELAT_1:74;

then A26: (max- f) | (E \ E3) = (max- g) | (E \ E3) by XBOOLE_1:33, RELAT_1:74;

Integral (M,(max- f)) = Integral (M,((max- f) | (E \ E3))) by A21, A22, A25, MESFUNC6:def 1, MESFUNC6:89;

then Integral (M,(max- f)) = Integral (M,(max- g)) by A26, A21, A22, A25, MESFUNC6:def 1, MESFUNC6:89;

then integral+ (M,(R_EAL (max- g))) < +infty by A21, A23, A24, MESFUNC6:61, MESFUNC6:82;

then integral+ (M,(max- (R_EAL g))) < +infty by Th43;

hence g is_integrable_on M by A12, A10, A5, A20, MESFUNC5:def 17, MESFUNC6:def 4; :: thesis: Integral (M,f) = Integral (M,g)

f | (E \ E0) = (f | (X \ E0)) | (E \ E0) by XBOOLE_1:33, RELAT_1:74;

then f | (E \ E0) = (f | (E0 `)) | (E \ E0) by SUBSET_1:def 4;

then f | (E \ E0) = (g | (X \ E0)) | (E \ E0) by A17, SUBSET_1:def 4;

then A27: f | (E \ E0) = g | (E \ E0) by XBOOLE_1:33, RELAT_1:74;

Integral (M,f) = Integral (M,(f | (E \ E0))) by A4, A10, A17, A7, MESFUNC6:def 1, MESFUNC6:89;

hence Integral (M,f) = Integral (M,g) by A5, A17, A27, A11, A1, A3, A4, Th26, MESFUNC6:89; :: thesis: verum

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 A2, MESFUNC6:def 4;

then consider E1 being Element of S such that

A7: ( E1 = dom (R_EAL f) & R_EAL f is E1 -measurable ) by MESFUNC5:def 17;

A8: integral+ (M,(max+ (R_EAL f))) < +infty by A6, MESFUNC5:def 17;

A9: integral+ (M,(max- (R_EAL f))) < +infty by A6, MESFUNC5:def 17;

A10: ( R_EAL f = f & R_EAL g = g ) by MESFUNC5:def 7;

then A11: f is E -measurable by A4, A7, MESFUNC6:def 1;

then A12: R_EAL g is E -measurable by A1, A3, A4, Th26, MESFUNC6:def 1;

A13: ( E = dom (max+ f) & E = dom (max+ g) ) by A4, A5, RFUNCT_3:def 10;

( max+ (R_EAL f) is E -measurable & max+ (R_EAL g) is E -measurable ) by A4, A7, A12, A10, A5, MESFUN11:10;

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 A13, MESFUNC6:61, MESFUNC6:82;

then A16: Integral (M,(max+ f)) < +infty by A8, Th43;

consider E0 being Element of S such that

A17: ( M . E0 = 0 & f | (E0 `) = g | (E0 `) ) by A3, LPSPACE1:def 10;

consider E2 being Element of S such that

A18: ( M . E2 = 0 & (max+ f) | (E2 `) = (max+ g) | (E2 `) ) by A3, Th42, LPSPACE1:def 10;

(max+ f) | (X \ E2) = (max+ f) | (E2 `) by SUBSET_1:def 4;

then (max+ f) | (X \ E2) = (max+ g) | (X \ E2) by A18, SUBSET_1:def 4;

then (max+ f) | (E \ E2) = ((max+ g) | (X \ E2)) | (E \ E2) by XBOOLE_1:33, RELAT_1:74;

then A19: (max+ f) | (E \ E2) = (max+ g) | (E \ E2) by XBOOLE_1:33, RELAT_1:74;

Integral (M,(max+ f)) = Integral (M,((max+ f) | (E \ E2))) by A13, A14, A18, MESFUNC6:def 1, MESFUNC6:89;

then Integral (M,(max+ f)) = Integral (M,(max+ g)) by A13, A14, A18, A19, MESFUNC6:def 1, MESFUNC6:89;

then integral+ (M,(R_EAL (max+ g))) < +infty by A13, A15, A16, MESFUNC6:61, MESFUNC6:82;

then A20: integral+ (M,(max+ (R_EAL g))) < +infty by Th43;

A21: ( E = dom (max- f) & E = dom (max- g) ) by A4, A5, RFUNCT_3:def 11;

( max- (R_EAL f) is E -measurable & max- (R_EAL g) is E -measurable ) by A4, A7, A12, A10, A5, MESFUN11:10;

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 A21, MESFUNC6:61, MESFUNC6:82;

then A24: Integral (M,(max- f)) < +infty by A9, Th43;

consider E3 being Element of S such that

A25: ( M . E3 = 0 & (max- f) | (E3 `) = (max- g) | (E3 `) ) by A3, Th42, LPSPACE1:def 10;

(max- f) | (X \ E3) = (max- f) | (E3 `) by SUBSET_1:def 4;

then (max- f) | (X \ E3) = (max- g) | (X \ E3) by A25, SUBSET_1:def 4;

then (max- f) | (E \ E3) = ((max- g) | (X \ E3)) | (E \ E3) by XBOOLE_1:33, RELAT_1:74;

then A26: (max- f) | (E \ E3) = (max- g) | (E \ E3) by XBOOLE_1:33, RELAT_1:74;

Integral (M,(max- f)) = Integral (M,((max- f) | (E \ E3))) by A21, A22, A25, MESFUNC6:def 1, MESFUNC6:89;

then Integral (M,(max- f)) = Integral (M,(max- g)) by A26, A21, A22, A25, MESFUNC6:def 1, MESFUNC6:89;

then integral+ (M,(R_EAL (max- g))) < +infty by A21, A23, A24, MESFUNC6:61, MESFUNC6:82;

then integral+ (M,(max- (R_EAL g))) < +infty by Th43;

hence g is_integrable_on M by A12, A10, A5, A20, MESFUNC5:def 17, MESFUNC6:def 4; :: thesis: Integral (M,f) = Integral (M,g)

f | (E \ E0) = (f | (X \ E0)) | (E \ E0) by XBOOLE_1:33, RELAT_1:74;

then f | (E \ E0) = (f | (E0 `)) | (E \ E0) by SUBSET_1:def 4;

then f | (E \ E0) = (g | (X \ E0)) | (E \ E0) by A17, SUBSET_1:def 4;

then A27: f | (E \ E0) = g | (E \ E0) by XBOOLE_1:33, RELAT_1:74;

Integral (M,f) = Integral (M,(f | (E \ E0))) by A4, A10, A17, A7, MESFUNC6:def 1, MESFUNC6:89;

hence Integral (M,f) = Integral (M,g) by A5, A17, A27, A11, A1, A3, A4, Th26, MESFUNC6:89; :: thesis: verum