let X be non empty set ; 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; 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; 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; 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; ( 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
; ( 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; 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; verum