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 ;
A5: f | (A `) = f | ((dom f) \ A) by Th15;
then A6: B = (dom f) /\ ((dom f) \ A) by
.= ((dom f) /\ (dom f)) \ A by XBOOLE_1:49
.= (dom f) \ A ;
then A7: dom f = A \/ B by ;
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 ;
defpred S1[ object ] means \$1 in A;
deffunc H1( object ) -> object = +infty ;
deffunc H2( 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
( ( S1[x] implies g . x = H1(x) ) & ( not S1[x] implies g . x = H2(x) ) ) ) ) from
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 b1 in ExtREAL )
assume y in rng g ; :: thesis:
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 ) ;
end;
end;
then rng g c= ExtREAL ;
then reconsider g = g as PartFunc of X,ExtREAL by ;
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 ;
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 ;
then (f | (A `)) . x = g . x by A9, A12, A13;
hence (f | (A `)) . x = (g | (A `)) . x by ; :: thesis: verum
end;
hence A14: f | (A `) = g | (A `) by ; :: 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 ;
then f | B = g | B by ;
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 ;
then A19: ( x in dom g & g . x < r ) by MESFUNC1:def 11;
A20: now :: thesis: not x in Aend;
then A21: x in B by ;
g . x = f . x by A9, A18, A20;
then (f | B) . x < r by ;
then x in less_dom ((f | B),r) by ;
hence x in B /\ (less_dom ((f | B),r)) by ; :: 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 ;
then g . x = f . x by A9;
then g . x < r by ;
then x in less_dom (g,r) by ;
hence x in (A \/ B) /\ (less_dom (g,r)) by ; :: 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 ;
A27: ( (max+ g) | B is nonnegative & (max- g) | B is nonnegative ) by ;
A28: ( dom (max+ g) = A \/ B & dom (max- g) = A \/ B ) by ;
A29: B = (A \/ B) /\ B by ;
then A30: ( dom ((max+ g) | B) = B & dom ((max- g) | B) = B ) by ;
A31: ( max+ g is B -measurable & max- g is B -measurable ) by ;
( Integral (M,((max+ g) | B)) = Integral (M,(max+ g)) & Integral (M,((max- g) | B)) = Integral (M,(max- g)) ) by ;
then ( integral+ (M,((max+ g) | B)) = Integral (M,(max+ g)) & integral+ (M,((max- g) | B)) = Integral (M,(max- g)) ) by ;
then ( integral+ (M,(max+ g)) < +infty & integral+ (M,(max- g)) < +infty ) by ;
hence g is_integrable_on M by ; :: 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 ;
hence Integral (M,(f | (A `))) = Integral (M,g) by ; :: thesis: verum