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 E -measurable ) & 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 E -measurable ) & 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 E -measurable ) & 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 E -measurable ) & 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 E -measurable ) & 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 E -measurable ) and

A2: f is nonnegative and

A3: 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

A4: E = dom f and

A5: f is E -measurable by A1;

ex C being Element of S st

( C = dom (f | A) & f | A is C -measurable )

ex C being Element of S st

( C = dom (f | (A \/ B)) & f | (A \/ B) is C -measurable )

A16: ex C being Element of S st

( C = dom (f | B) & f | B is C -measurable )

hence Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B))) by A2, A15, A10, A16, Th15, Th88; :: thesis: verum

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 E -measurable ) & 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 E -measurable ) & 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 E -measurable ) & 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 E -measurable ) & 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 E -measurable ) & 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 E -measurable ) and

A2: f is nonnegative and

A3: 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

A4: E = dom f and

A5: f is E -measurable by A1;

ex C being Element of S st

( C = dom (f | A) & f | A is C -measurable )

proof

then A10:
Integral (M,(f | A)) = integral+ (M,(f | A))
by A2, Th15, Th88;
take C = E /\ A; :: thesis: ( C = dom (f | A) & f | A is C -measurable )

thus dom (f | A) = C by A4, RELAT_1:61; :: thesis: f | A is C -measurable

A6: C = (dom f) /\ C by A4, XBOOLE_1:17, XBOOLE_1:28;

A7: dom (f | A) = C by A4, RELAT_1:61

.= dom (f | C) by A6, RELAT_1:61 ;

for x being object st x in dom (f | A) holds

(f | A) . x = (f | C) . x

f is C -measurable by A5, MESFUNC1:30, XBOOLE_1:17;

hence f | A is C -measurable by A6, A9, Th42; :: thesis: verum

end;thus dom (f | A) = C by A4, RELAT_1:61; :: thesis: f | A is C -measurable

A6: C = (dom f) /\ C by A4, XBOOLE_1:17, XBOOLE_1:28;

A7: dom (f | A) = C by A4, RELAT_1:61

.= dom (f | C) by A6, RELAT_1:61 ;

for x being object st x in dom (f | A) holds

(f | A) . x = (f | C) . x

proof

then A9:
f | C = f | A
by A7, FUNCT_1:2;
let x be object ; :: thesis: ( x in dom (f | A) implies (f | A) . x = (f | C) . x )

assume A8: x in dom (f | A) ; :: thesis: (f | A) . x = (f | C) . x

then (f | A) . x = f . x by FUNCT_1:47;

hence (f | A) . x = (f | C) . x by A7, A8, FUNCT_1:47; :: thesis: verum

end;assume A8: x in dom (f | A) ; :: thesis: (f | A) . x = (f | C) . x

then (f | A) . x = f . x by FUNCT_1:47;

hence (f | A) . x = (f | C) . x by A7, A8, FUNCT_1:47; :: thesis: verum

f is C -measurable by A5, MESFUNC1:30, XBOOLE_1:17;

hence f | A is C -measurable by A6, A9, Th42; :: thesis: verum

ex C being Element of S st

( C = dom (f | (A \/ B)) & f | (A \/ B) is C -measurable )

proof

then A15:
Integral (M,(f | (A \/ B))) = integral+ (M,(f | (A \/ B)))
by A2, Th15, Th88;
reconsider C = E /\ (A \/ B) as Element of S ;

take C ; :: thesis: ( C = dom (f | (A \/ B)) & f | (A \/ B) is C -measurable )

thus dom (f | (A \/ B)) = C by A4, RELAT_1:61; :: thesis: f | (A \/ B) is C -measurable

A11: C = (dom f) /\ C by A4, XBOOLE_1:17, XBOOLE_1:28;

A12: dom (f | (A \/ B)) = C by A4, RELAT_1:61

.= dom (f | C) by A11, RELAT_1:61 ;

A13: for x being object st x in dom (f | (A \/ B)) holds

(f | (A \/ B)) . x = (f | C) . x

then f | C is C -measurable by A11, Th42;

hence f | (A \/ B) is C -measurable by A12, A13, FUNCT_1:2; :: thesis: verum

end;take C ; :: thesis: ( C = dom (f | (A \/ B)) & f | (A \/ B) is C -measurable )

thus dom (f | (A \/ B)) = C by A4, RELAT_1:61; :: thesis: f | (A \/ B) is C -measurable

A11: C = (dom f) /\ C by A4, XBOOLE_1:17, XBOOLE_1:28;

A12: dom (f | (A \/ B)) = C by A4, RELAT_1:61

.= dom (f | C) by A11, RELAT_1:61 ;

A13: for x being object st x in dom (f | (A \/ B)) holds

(f | (A \/ B)) . x = (f | C) . x

proof

f is C -measurable
by A5, MESFUNC1:30, XBOOLE_1:17;
let x be object ; :: thesis: ( x in dom (f | (A \/ B)) implies (f | (A \/ B)) . x = (f | C) . x )

assume A14: x in dom (f | (A \/ B)) ; :: thesis: (f | (A \/ B)) . x = (f | C) . x

then (f | (A \/ B)) . x = f . x by FUNCT_1:47;

hence (f | (A \/ B)) . x = (f | C) . x by A12, A14, FUNCT_1:47; :: thesis: verum

end;assume A14: x in dom (f | (A \/ B)) ; :: thesis: (f | (A \/ B)) . x = (f | C) . x

then (f | (A \/ B)) . x = f . x by FUNCT_1:47;

hence (f | (A \/ B)) . x = (f | C) . x by A12, A14, FUNCT_1:47; :: thesis: verum

then f | C is C -measurable by A11, Th42;

hence f | (A \/ B) is C -measurable by A12, A13, FUNCT_1:2; :: thesis: verum

A16: ex C being Element of S st

( C = dom (f | B) & f | B is C -measurable )

proof

integral+ (M,(f | (A \/ B))) = (integral+ (M,(f | A))) + (integral+ (M,(f | B)))
by A1, A2, A3, Th81;
take C = E /\ B; :: thesis: ( C = dom (f | B) & f | B is C -measurable )

thus dom (f | B) = C by A4, RELAT_1:61; :: thesis: f | B is C -measurable

A17: C = (dom f) /\ C by A4, XBOOLE_1:17, XBOOLE_1:28;

A18: dom (f | B) = C by A4, RELAT_1:61

.= dom (f | C) by A17, RELAT_1:61 ;

for x being object st x in dom (f | B) holds

(f | B) . x = (f | C) . x

f is C -measurable by A5, MESFUNC1:30, XBOOLE_1:17;

hence f | B is C -measurable by A17, A20, Th42; :: thesis: verum

end;thus dom (f | B) = C by A4, RELAT_1:61; :: thesis: f | B is C -measurable

A17: C = (dom f) /\ C by A4, XBOOLE_1:17, XBOOLE_1:28;

A18: dom (f | B) = C by A4, RELAT_1:61

.= dom (f | C) by A17, RELAT_1:61 ;

for x being object st x in dom (f | B) holds

(f | B) . x = (f | C) . x

proof

then A20:
f | C = f | B
by A18, FUNCT_1:2;
let x be object ; :: 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:47;

hence (f | B) . x = (f | C) . x by A18, A19, FUNCT_1:47; :: thesis: verum

end;assume A19: x in dom (f | B) ; :: thesis: (f | B) . x = (f | C) . x

then (f | B) . x = f . x by FUNCT_1:47;

hence (f | B) . x = (f | C) . x by A18, A19, FUNCT_1:47; :: thesis: verum

f is C -measurable by A5, MESFUNC1:30, XBOOLE_1:17;

hence f | B is C -measurable by A17, A20, Th42; :: thesis: verum

hence Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B))) by A2, A15, A10, A16, Th15, Th88; :: thesis: verum