let X be non empty set ; 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; 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; 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; 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; ( 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
; 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
take C =
E /\ A;
( C = dom (f | A) & f | A is C -measurable )
thus
dom (f | A) = C
by A4, RELAT_1:61;
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
then A9:
f | C = f | A
by A7, FUNCT_1:2;
f is
C -measurable
by A5, MESFUNC1:30, XBOOLE_1:17;
hence
f | A is
C -measurable
by A6, A9, Th42;
verum
end;
then A10:
Integral (M,(f | A)) = integral+ (M,(f | A))
by A2, Th15, Th88;
ex C being Element of S st
( C = dom (f | (A \/ B)) & f | (A \/ B) is C -measurable )
proof
reconsider C =
E /\ (A \/ B) as
Element of
S ;
take
C
;
( C = dom (f | (A \/ B)) & f | (A \/ B) is C -measurable )
thus
dom (f | (A \/ B)) = C
by A4, RELAT_1:61;
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
f is
C -measurable
by A5, MESFUNC1:30, XBOOLE_1:17;
then
f | C is
C -measurable
by A11, Th42;
hence
f | (A \/ B) is
C -measurable
by A12, A13, FUNCT_1:2;
verum
end;
then A15:
Integral (M,(f | (A \/ B))) = integral+ (M,(f | (A \/ B)))
by A2, Th15, Th88;
A16:
ex C being Element of S st
( C = dom (f | B) & f | B is C -measurable )
proof
take C =
E /\ B;
( C = dom (f | B) & f | B is C -measurable )
thus
dom (f | B) = C
by A4, RELAT_1:61;
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
then A20:
f | C = f | B
by A18, FUNCT_1:2;
f is
C -measurable
by A5, MESFUNC1:30, XBOOLE_1:17;
hence
f | B is
C -measurable
by A17, A20, Th42;
verum
end;
integral+ (M,(f | (A \/ B))) = (integral+ (M,(f | A))) + (integral+ (M,(f | B)))
by A1, A2, A3, Th81;
hence
Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B)))
by A2, A15, A10, A16, Th15, Th88; verum