let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for A, B being Element of S st ex E being Element of S st
( E = dom f & f is_measurable_on E ) & f is nonnegative & A misses B holds
Integral M,(f | (A \/ B)) = (Integral M,(f | A)) + (Integral M,(f | B))
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for A, B being Element of S st ex E being Element of S st
( E = dom f & f is_measurable_on E ) & f is nonnegative & A misses B holds
Integral M,(f | (A \/ B)) = (Integral M,(f | A)) + (Integral M,(f | B))
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL
for A, B being Element of S st ex E being Element of S st
( E = dom f & f is_measurable_on E ) & f is nonnegative & A misses B holds
Integral M,(f | (A \/ B)) = (Integral M,(f | A)) + (Integral M,(f | B))
let f be PartFunc of X,ExtREAL ; :: thesis: for A, B being Element of S st ex E being Element of S st
( E = dom f & f is_measurable_on E ) & f is nonnegative & A misses B holds
Integral M,(f | (A \/ B)) = (Integral M,(f | A)) + (Integral M,(f | B))
let A, B be Element of S; :: thesis: ( ex E being Element of S st
( E = dom f & f is_measurable_on E ) & f is nonnegative & A misses B implies Integral M,(f | (A \/ B)) = (Integral M,(f | A)) + (Integral M,(f | B)) )
assume that
A1: ex E being Element of S st
( E = dom f & f is_measurable_on E ) and
A2: ( f is nonnegative & A misses B ) ; :: thesis: Integral M,(f | (A \/ B)) = (Integral M,(f | A)) + (Integral M,(f | B))
consider E being Element of S such that
A3: ( E = dom f & f is_measurable_on E ) by A1;
A4: ex C being Element of S st
( C = dom (f | (A \/ B)) & f | (A \/ B) is_measurable_on C )

proof

reconsider C = E /\ (A \/ B) as Element of S ;
take C ; :: thesis: ( C = dom (f | (A \/ B)) & f | (A \/ B) is_measurable_on C )
thus dom (f | (A \/ B)) = C by A3, RELAT_1:90; :: thesis: f | (A \/ B) is_measurable_on C
C c= dom f by A3, XBOOLE_1:17;
then A5: ( f is_measurable_on C & C = (dom f) /\ C ) by A3, MESFUNC1:34, XBOOLE_1:28;
then A6: f | C is_measurable_on C by Th48;
A7: dom (f | (A \/ B)) = C by A3, RELAT_1:90
.= dom (f | C) by A5, RELAT_1:90 ;
for x being set st x in dom (f | (A \/ B)) holds
(f | (A \/ B)) . x = (f | C) . x

proof

let x be set ; :: thesis: ( x in dom (f | (A \/ B)) implies (f | (A \/ B)) . x = (f | C) . x )
assume A8: x in dom (f | (A \/ B)) ; :: thesis: (f | (A \/ B)) . x = (f | C) . x
then (f | (A \/ B)) . x = f . x by FUNCT_1:70;
hence (f | (A \/ B)) . x = (f | C) . x by A7, A8, FUNCT_1:70; :: thesis: verum

end;

hence f | (A \/ B) is_measurable_on C by A6, A7, FUNCT_1:9; :: thesis: verum

end;

A9: integral+ M,(f | (A \/ B)) = (integral+ M,(f | A)) + (integral+ M,(f | B)) by A1, A2, Th87;
A10: Integral M,(f | (A \/ B)) = integral+ M,(f | (A \/ B)) by A2, A4, Th21, Th94;
ex C being Element of S st
( C = dom (f | A) & f | A is_measurable_on C )

proof

take C = E /\ A; :: thesis: ( C = dom (f | A) & f | A is_measurable_on C )
thus dom (f | A) = C by A3, RELAT_1:90; :: thesis: f | A is_measurable_on C
A11: f is_measurable_on C by A3, MESFUNC1:34, XBOOLE_1:17;
A12: C = (dom f) /\ C by A3, XBOOLE_1:17, XBOOLE_1:28;
A13: dom (f | A) = C by A3, RELAT_1:90
.= dom (f | C) by A12, RELAT_1:90 ;
for x being set st x in dom (f | A) holds
(f | A) . x = (f | C) . x

proof

let x be set ; :: thesis: ( x in dom (f | A) implies (f | A) . x = (f | C) . x )
assume A14: x in dom (f | A) ; :: thesis: (f | A) . x = (f | C) . x
then (f | A) . x = f . x by FUNCT_1:70;
hence (f | A) . x = (f | C) . x by A13, A14, FUNCT_1:70; :: thesis: verum

end;

then f | C = f | A by A13, FUNCT_1:9;
hence f | A is_measurable_on C by A11, A12, Th48; :: thesis: verum

end;

then A15: Integral M,(f | A) = integral+ M,(f | A) by A2, Th21, Th94;
ex C being Element of S st
( C = dom (f | B) & f | B is_measurable_on C )

proof

take C = E /\ B; :: thesis: ( C = dom (f | B) & f | B is_measurable_on C )
thus dom (f | B) = C by A3, RELAT_1:90; :: thesis: f | B is_measurable_on C
A16: f is_measurable_on C by A3, MESFUNC1:34, XBOOLE_1:17;
A17: C = (dom f) /\ C by A3, XBOOLE_1:17, XBOOLE_1:28;
A18: dom (f | B) = C by A3, RELAT_1:90
.= dom (f | C) by A17, RELAT_1:90 ;
for x being set st x in dom (f | B) holds
(f | B) . x = (f | C) . x

proof

let x be set ; :: thesis: ( x in dom (f | B) implies (f | B) . x = (f | C) . x )
assume A19: x in dom (f | B) ; :: thesis: (f | B) . x = (f | C) . x
then (f | B) . x = f . x by FUNCT_1:70;
hence (f | B) . x = (f | C) . x by A18, A19, FUNCT_1:70; :: thesis: verum

end;

then f | C = f | B by A18, FUNCT_1:9;
hence f | B is_measurable_on C by A16, A17, Th48; :: thesis: verum

end;

hence Integral M,(f | (A \/ B)) = (Integral M,(f | A)) + (Integral M,(f | B)) by A2, A9, A10, A15, Th21, Th94; :: thesis: verum