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₁[ object ] means $1 in A;
deffunc H₁( object ) -> object = +infty ;
deffunc H₂( 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₁[x] implies g . x = H₁(x) ) & ( not S₁[x] implies g . x = H₂(x) ) ) ) ) from PARTFUN1:sch 1();

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

let y be object ; :: thesis: ( y in rng g implies b₁ in ExtREAL )
assume y in rng g ; :: thesis: b₁ in ExtREAL
then consider x being object such that
A10: ( x in dom g & y = g . x ) by FUNCT_1:def 3;

per cases ( x in A or not x in A ) ;

suppose x in A ; :: thesis: b₁ in ExtREAL

then g . x = +infty by A9, A10;
hence y in ExtREAL by A10, XXREAL_0:def 1; :: thesis: verum

end;

suppose not x in A ; :: thesis: b₁ in ExtREAL

then g . x = f . x by A9, A10;
then g . x in rng f by A9, A10, FUNCT_1:3;
hence y in ExtREAL by A10; :: thesis: verum

end;

end;

end;

then rng g c= ExtREAL ;
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

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;

hence A14: f | (A `) = g | (A `) by A11, PARTFUN1:5; :: thesis: ( g is_integrable_on M & Integral (M,(f | (A `))) = Integral (M,g) )
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

let r be Real; :: thesis: (A \/ B) /\ (less_dom (g,r)) in S

now :: thesis: for x being object st x in (A \/ B) /\ (less_dom (g,r)) holds
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;

A20: now :: thesis: not x in A

assume x in A ; :: thesis: contradiction
then g . x = +infty by A9, A18;
hence contradiction by A19, XXREAL_0:3; :: thesis: verum

end;

then A21: x in B by A7, A18, XBOOLE_0:def 3;
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;

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

now :: thesis: for x being object st x in B /\ (less_dom ((f | B),r)) holds
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;

then B /\ (less_dom ((f | B),r)) c= (A \/ B) /\ (less_dom (g,r)) ;
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;

then A26: ( max+ g is A \/ B -measurable & max- g is A \/ B -measurable ) by A7, A9, MESFUNC1:def 16, MESFUNC2:25, MESFUNC2:26;
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