let X be non empty set ; :: thesis: for S being SigmaField of X

for M being sigma_Measure of S

for A being Element of S

for f being PartFunc of X,ExtREAL st M . A = 0 & A c= dom f & f | (A `) is_integrable_on M holds

ex g being PartFunc of X,ExtREAL st

( dom g = dom f & f | (A `) = g | (A `) & g is_integrable_on M & Integral (M,(f | (A `))) = Integral (M,g) )

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for A being Element of S

for f being PartFunc of X,ExtREAL st M . A = 0 & A c= dom f & f | (A `) is_integrable_on M holds

ex g being PartFunc of X,ExtREAL st

( dom g = dom f & f | (A `) = g | (A `) & g is_integrable_on M & Integral (M,(f | (A `))) = Integral (M,g) )

let M be sigma_Measure of S; :: thesis: for A being Element of S

for f being PartFunc of X,ExtREAL st M . A = 0 & A c= dom f & f | (A `) is_integrable_on M holds

ex g being PartFunc of X,ExtREAL st

( dom g = dom f & f | (A `) = g | (A `) & g is_integrable_on M & Integral (M,(f | (A `))) = Integral (M,g) )

let A be Element of S; :: thesis: for f being PartFunc of X,ExtREAL st M . A = 0 & A c= dom f & f | (A `) is_integrable_on M holds

ex g being PartFunc of X,ExtREAL st

( dom g = dom f & f | (A `) = g | (A `) & g is_integrable_on M & Integral (M,(f | (A `))) = Integral (M,g) )

let f be PartFunc of X,ExtREAL; :: thesis: ( M . A = 0 & A c= dom f & f | (A `) is_integrable_on M implies ex g being PartFunc of X,ExtREAL st

( dom g = dom f & f | (A `) = g | (A `) & g is_integrable_on M & Integral (M,(f | (A `))) = Integral (M,g) ) )

assume that

A2: M . A = 0 and

A1: A c= dom f and

A3: f | (A `) is_integrable_on M ; :: thesis: ex g being PartFunc of X,ExtREAL st

( dom g = dom f & f | (A `) = g | (A `) & g is_integrable_on M & Integral (M,(f | (A `))) = Integral (M,g) )

consider B being Element of S such that

A4: ( B = dom (f | (A `)) & f | (A `) is B -measurable ) by A3, MESFUNC5:def 17;

A5: f | (A `) = f | ((dom f) \ A) by Th15;

then A6: B = (dom f) /\ ((dom f) \ A) by A4, RELAT_1:61

.= ((dom f) /\ (dom f)) \ A by XBOOLE_1:49

.= (dom f) \ A ;

then A7: dom f = A \/ B by A1, XBOOLE_1:45;

A8: ( ex E being Element of S st

( E = dom (f | B) & f | B is E -measurable ) & integral+ (M,(max+ (f | B))) < +infty & integral+ (M,(max- (f | B))) < +infty ) by A3, A5, A6, MESFUNC5:def 17;

defpred S_{1}[ object ] means $1 in A;

deffunc H_{1}( object ) -> object = +infty ;

deffunc H_{2}( object ) -> set = f . $1;

consider g being Function such that

A9: ( dom g = dom f & ( for x being object st x in dom f holds

( ( S_{1}[x] implies g . x = H_{1}(x) ) & ( not S_{1}[x] implies g . x = H_{2}(x) ) ) ) )
from PARTFUN1:sch 1();

then reconsider g = g as PartFunc of X,ExtREAL by A9, RELSET_1:4;

take g ; :: thesis: ( dom g = dom f & f | (A `) = g | (A `) & g is_integrable_on M & Integral (M,(f | (A `))) = Integral (M,g) )

thus dom g = dom f by A9; :: thesis: ( f | (A `) = g | (A `) & g is_integrable_on M & Integral (M,(f | (A `))) = Integral (M,g) )

dom (f | (A `)) = (dom f) /\ (A `) by RELAT_1:61;

then A11: dom (f | (A `)) = dom (g | (A `)) by A9, RELAT_1:61;

A15: A ` = X \ A by SUBSET_1:def 4;

then f | B = (g | (A `)) | B by A6, A14, XBOOLE_1:33, RELAT_1:74;

then f | B = g | B by A6, A15, XBOOLE_1:33, RELAT_1:74;

then A16: ( (max+ g) | B = max+ (f | B) & (max- g) | B = max- (f | B) ) by MESFUNC5:28;

A17: for r being Real holds (A \/ B) /\ (less_dom (g,r)) in S

A27: ( (max+ g) | B is nonnegative & (max- g) | B is nonnegative ) by MESFUNC5:15, MESFUN11:5;

A28: ( dom (max+ g) = A \/ B & dom (max- g) = A \/ B ) by A7, A9, MESFUNC2:def 2, MESFUNC2:def 3;

A29: B = (A \/ B) /\ B by XBOOLE_1:7, XBOOLE_1:28;

then A30: ( dom ((max+ g) | B) = B & dom ((max- g) | B) = B ) by A28, RELAT_1:61;

A31: ( max+ g is B -measurable & max- g is B -measurable ) by A26, XBOOLE_1:7, MESFUNC1:30;

( Integral (M,((max+ g) | B)) = Integral (M,(max+ g)) & Integral (M,((max- g) | B)) = Integral (M,(max- g)) ) by A2, A6, A7, A26, A28, MESFUNC5:95;

then ( integral+ (M,((max+ g) | B)) = Integral (M,(max+ g)) & integral+ (M,((max- g) | B)) = Integral (M,(max- g)) ) by A27, A28, A29, A30, A31, MESFUNC5:42, MESFUNC5:88;

then ( integral+ (M,(max+ g)) < +infty & integral+ (M,(max- g)) < +infty ) by A8, A16, A26, A28, MESFUNC5:88, MESFUN11:5;

hence g is_integrable_on M by A7, A9, A17, MESFUNC5:def 17, MESFUNC1:def 16; :: thesis: Integral (M,(f | (A `))) = Integral (M,g)

f is_a.e.integrable_on M by A1, A2, A3;

then reconsider E = dom f as Element of S by Th16;

Integral (M,(f | (A `))) = Integral (M,(g | ((dom g) \ A))) by A14, Th15;

hence Integral (M,(f | (A `))) = Integral (M,g) by A2, A7, A9, A17, MESFUNC5:95, MESFUNC1:def 16; :: thesis: verum

for M being sigma_Measure of S

for A being Element of S

for f being PartFunc of X,ExtREAL st M . A = 0 & A c= dom f & f | (A `) is_integrable_on M holds

ex g being PartFunc of X,ExtREAL st

( dom g = dom f & f | (A `) = g | (A `) & g is_integrable_on M & Integral (M,(f | (A `))) = Integral (M,g) )

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for A being Element of S

for f being PartFunc of X,ExtREAL st M . A = 0 & A c= dom f & f | (A `) is_integrable_on M holds

ex g being PartFunc of X,ExtREAL st

( dom g = dom f & f | (A `) = g | (A `) & g is_integrable_on M & Integral (M,(f | (A `))) = Integral (M,g) )

let M be sigma_Measure of S; :: thesis: for A being Element of S

for f being PartFunc of X,ExtREAL st M . A = 0 & A c= dom f & f | (A `) is_integrable_on M holds

ex g being PartFunc of X,ExtREAL st

( dom g = dom f & f | (A `) = g | (A `) & g is_integrable_on M & Integral (M,(f | (A `))) = Integral (M,g) )

let A be Element of S; :: thesis: for f being PartFunc of X,ExtREAL st M . A = 0 & A c= dom f & f | (A `) is_integrable_on M holds

ex g being PartFunc of X,ExtREAL st

( dom g = dom f & f | (A `) = g | (A `) & g is_integrable_on M & Integral (M,(f | (A `))) = Integral (M,g) )

let f be PartFunc of X,ExtREAL; :: thesis: ( M . A = 0 & A c= dom f & f | (A `) is_integrable_on M implies ex g being PartFunc of X,ExtREAL st

( dom g = dom f & f | (A `) = g | (A `) & g is_integrable_on M & Integral (M,(f | (A `))) = Integral (M,g) ) )

assume that

A2: M . A = 0 and

A1: A c= dom f and

A3: f | (A `) is_integrable_on M ; :: thesis: ex g being PartFunc of X,ExtREAL st

( dom g = dom f & f | (A `) = g | (A `) & g is_integrable_on M & Integral (M,(f | (A `))) = Integral (M,g) )

consider B being Element of S such that

A4: ( B = dom (f | (A `)) & f | (A `) is B -measurable ) by A3, MESFUNC5:def 17;

A5: f | (A `) = f | ((dom f) \ A) by Th15;

then A6: B = (dom f) /\ ((dom f) \ A) by A4, RELAT_1:61

.= ((dom f) /\ (dom f)) \ A by XBOOLE_1:49

.= (dom f) \ A ;

then A7: dom f = A \/ B by A1, XBOOLE_1:45;

A8: ( ex E being Element of S st

( E = dom (f | B) & f | B is E -measurable ) & integral+ (M,(max+ (f | B))) < +infty & integral+ (M,(max- (f | B))) < +infty ) by A3, A5, A6, MESFUNC5:def 17;

defpred S

deffunc H

deffunc H

consider g being Function such that

A9: ( dom g = dom f & ( for x being object st x in dom f holds

( ( S

now :: thesis: for y being object st y in rng g holds

y in ExtREAL

then
rng g c= ExtREAL
;y in ExtREAL

let y be object ; :: thesis: ( y in rng g implies b_{1} in ExtREAL )

assume y in rng g ; :: thesis: b_{1} in ExtREAL

then consider x being object such that

A10: ( x in dom g & y = g . x ) by FUNCT_1:def 3;

end;assume y in rng g ; :: thesis: b

then consider x being object such that

A10: ( x in dom g & y = g . x ) by FUNCT_1:def 3;

then reconsider g = g as PartFunc of X,ExtREAL by A9, RELSET_1:4;

take g ; :: thesis: ( dom g = dom f & f | (A `) = g | (A `) & g is_integrable_on M & Integral (M,(f | (A `))) = Integral (M,g) )

thus dom g = dom f by A9; :: thesis: ( f | (A `) = g | (A `) & g is_integrable_on M & Integral (M,(f | (A `))) = Integral (M,g) )

dom (f | (A `)) = (dom f) /\ (A `) by RELAT_1:61;

then A11: dom (f | (A `)) = dom (g | (A `)) by A9, RELAT_1:61;

now :: thesis: for x being Element of X st x in dom (f | (A `)) holds

(f | (A `)) . x = (g | (A `)) . x

hence A14:
f | (A `) = g | (A `)
by A11, PARTFUN1:5; :: thesis: ( g is_integrable_on M & Integral (M,(f | (A `))) = Integral (M,g) )(f | (A `)) . x = (g | (A `)) . x

let x be Element of X; :: thesis: ( x in dom (f | (A `)) implies (f | (A `)) . x = (g | (A `)) . x )

assume x in dom (f | (A `)) ; :: thesis: (f | (A `)) . x = (g | (A `)) . x

then A12: ( x in dom f & x in A ` ) by RELAT_1:57;

then x in X \ A by SUBSET_1:def 4;

then A13: not x in A by XBOOLE_0:def 5;

(f | (A `)) . x = f . x by A12, FUNCT_1:49;

then (f | (A `)) . x = g . x by A9, A12, A13;

hence (f | (A `)) . x = (g | (A `)) . x by A12, FUNCT_1:49; :: thesis: verum

end;assume x in dom (f | (A `)) ; :: thesis: (f | (A `)) . x = (g | (A `)) . x

then A12: ( x in dom f & x in A ` ) by RELAT_1:57;

then x in X \ A by SUBSET_1:def 4;

then A13: not x in A by XBOOLE_0:def 5;

(f | (A `)) . x = f . x by A12, FUNCT_1:49;

then (f | (A `)) . x = g . x by A9, A12, A13;

hence (f | (A `)) . x = (g | (A `)) . x by A12, FUNCT_1:49; :: thesis: verum

A15: A ` = X \ A by SUBSET_1:def 4;

then f | B = (g | (A `)) | B by A6, A14, XBOOLE_1:33, RELAT_1:74;

then f | B = g | B by A6, A15, XBOOLE_1:33, RELAT_1:74;

then A16: ( (max+ g) | B = max+ (f | B) & (max- g) | B = max- (f | B) ) by MESFUNC5:28;

A17: for r being Real holds (A \/ B) /\ (less_dom (g,r)) in S

proof

then A26:
( max+ g is A \/ B -measurable & max- g is A \/ B -measurable )
by A7, A9, MESFUNC1:def 16, MESFUNC2:25, MESFUNC2:26;
let r be Real; :: thesis: (A \/ B) /\ (less_dom (g,r)) in S

then (A \/ B) /\ (less_dom (g,r)) = B /\ (less_dom ((f | B),r)) by A22;

hence (A \/ B) /\ (less_dom (g,r)) in S by A4, A5, A6; :: thesis: verum

end;now :: thesis: for x being object st x in (A \/ B) /\ (less_dom (g,r)) holds

x in B /\ (less_dom ((f | B),r))

then A22:
(A \/ B) /\ (less_dom (g,r)) c= B /\ (less_dom ((f | B),r))
;x in B /\ (less_dom ((f | B),r))

let x be object ; :: thesis: ( x in (A \/ B) /\ (less_dom (g,r)) implies x in B /\ (less_dom ((f | B),r)) )

assume x in (A \/ B) /\ (less_dom (g,r)) ; :: thesis: x in B /\ (less_dom ((f | B),r))

then A18: ( x in dom f & x in less_dom (g,r) ) by A7, XBOOLE_0:def 4;

then A19: ( x in dom g & g . x < r ) by MESFUNC1:def 11;

g . x = f . x by A9, A18, A20;

then (f | B) . x < r by A19, A21, FUNCT_1:49;

then x in less_dom ((f | B),r) by A4, A5, A6, A21, MESFUNC1:def 11;

hence x in B /\ (less_dom ((f | B),r)) by A21, XBOOLE_0:def 4; :: thesis: verum

end;assume x in (A \/ B) /\ (less_dom (g,r)) ; :: thesis: x in B /\ (less_dom ((f | B),r))

then A18: ( x in dom f & x in less_dom (g,r) ) by A7, XBOOLE_0:def 4;

then A19: ( x in dom g & g . x < r ) by MESFUNC1:def 11;

A20: now :: thesis: not x in A

then A21:
x in B
by A7, A18, XBOOLE_0:def 3;assume
x in A
; :: thesis: contradiction

then g . x = +infty by A9, A18;

hence contradiction by A19, XXREAL_0:3; :: thesis: verum

end;then g . x = +infty by A9, A18;

hence contradiction by A19, XXREAL_0:3; :: thesis: verum

g . x = f . x by A9, A18, A20;

then (f | B) . x < r by A19, A21, FUNCT_1:49;

then x in less_dom ((f | B),r) by A4, A5, A6, A21, MESFUNC1:def 11;

hence x in B /\ (less_dom ((f | B),r)) by A21, XBOOLE_0:def 4; :: thesis: verum

now :: thesis: for x being object st x in B /\ (less_dom ((f | B),r)) holds

x in (A \/ B) /\ (less_dom (g,r))

then
B /\ (less_dom ((f | B),r)) c= (A \/ B) /\ (less_dom (g,r))
;x in (A \/ B) /\ (less_dom (g,r))

let x be object ; :: thesis: ( x in B /\ (less_dom ((f | B),r)) implies x in (A \/ B) /\ (less_dom (g,r)) )

assume x in B /\ (less_dom ((f | B),r)) ; :: thesis: x in (A \/ B) /\ (less_dom (g,r))

then A23: ( x in B & x in less_dom ((f | B),r) ) by XBOOLE_0:def 4;

then A24: ( x in dom (f | B) & (f | B) . x < r ) by MESFUNC1:def 11;

A25: ( x in dom f & not x in A ) by A23, A6, XBOOLE_0:def 5;

then g . x = f . x by A9;

then g . x < r by A24, FUNCT_1:47;

then x in less_dom (g,r) by A9, A25, MESFUNC1:def 11;

hence x in (A \/ B) /\ (less_dom (g,r)) by A7, A25, XBOOLE_0:def 4; :: thesis: verum

end;assume x in B /\ (less_dom ((f | B),r)) ; :: thesis: x in (A \/ B) /\ (less_dom (g,r))

then A23: ( x in B & x in less_dom ((f | B),r) ) by XBOOLE_0:def 4;

then A24: ( x in dom (f | B) & (f | B) . x < r ) by MESFUNC1:def 11;

A25: ( x in dom f & not x in A ) by A23, A6, XBOOLE_0:def 5;

then g . x = f . x by A9;

then g . x < r by A24, FUNCT_1:47;

then x in less_dom (g,r) by A9, A25, MESFUNC1:def 11;

hence x in (A \/ B) /\ (less_dom (g,r)) by A7, A25, XBOOLE_0:def 4; :: thesis: verum

then (A \/ B) /\ (less_dom (g,r)) = B /\ (less_dom ((f | B),r)) by A22;

hence (A \/ B) /\ (less_dom (g,r)) in S by A4, A5, A6; :: thesis: verum

A27: ( (max+ g) | B is nonnegative & (max- g) | B is nonnegative ) by MESFUNC5:15, MESFUN11:5;

A28: ( dom (max+ g) = A \/ B & dom (max- g) = A \/ B ) by A7, A9, MESFUNC2:def 2, MESFUNC2:def 3;

A29: B = (A \/ B) /\ B by XBOOLE_1:7, XBOOLE_1:28;

then A30: ( dom ((max+ g) | B) = B & dom ((max- g) | B) = B ) by A28, RELAT_1:61;

A31: ( max+ g is B -measurable & max- g is B -measurable ) by A26, XBOOLE_1:7, MESFUNC1:30;

( Integral (M,((max+ g) | B)) = Integral (M,(max+ g)) & Integral (M,((max- g) | B)) = Integral (M,(max- g)) ) by A2, A6, A7, A26, A28, MESFUNC5:95;

then ( integral+ (M,((max+ g) | B)) = Integral (M,(max+ g)) & integral+ (M,((max- g) | B)) = Integral (M,(max- g)) ) by A27, A28, A29, A30, A31, MESFUNC5:42, MESFUNC5:88;

then ( integral+ (M,(max+ g)) < +infty & integral+ (M,(max- g)) < +infty ) by A8, A16, A26, A28, MESFUNC5:88, MESFUN11:5;

hence g is_integrable_on M by A7, A9, A17, MESFUNC5:def 17, MESFUNC1:def 16; :: thesis: Integral (M,(f | (A `))) = Integral (M,g)

f is_a.e.integrable_on M by A1, A2, A3;

then reconsider E = dom f as Element of S by Th16;

Integral (M,(f | (A `))) = Integral (M,(g | ((dom g) \ A))) by A14, Th15;

hence Integral (M,(f | (A `))) = Integral (M,g) by A2, A7, A9, A17, MESFUNC5:95, MESFUNC1:def 16; :: thesis: verum