let X1, X2 be non empty set ; for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for E, A, B being Element of sigma (measurable_rectangles (S1,S2))
for f being PartFunc of [:X1,X2:],ExtREAL st E = dom f & f is nonnegative & f is E -measurable & A misses B holds
( Integral1 (M1,(f | (A \/ B))) = (Integral1 (M1,(f | A))) + (Integral1 (M1,(f | B))) & Integral2 (M2,(f | (A \/ B))) = (Integral2 (M2,(f | A))) + (Integral2 (M2,(f | B))) )
let S1 be SigmaField of X1; for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for E, A, B being Element of sigma (measurable_rectangles (S1,S2))
for f being PartFunc of [:X1,X2:],ExtREAL st E = dom f & f is nonnegative & f is E -measurable & A misses B holds
( Integral1 (M1,(f | (A \/ B))) = (Integral1 (M1,(f | A))) + (Integral1 (M1,(f | B))) & Integral2 (M2,(f | (A \/ B))) = (Integral2 (M2,(f | A))) + (Integral2 (M2,(f | B))) )
let S2 be SigmaField of X2; for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for E, A, B being Element of sigma (measurable_rectangles (S1,S2))
for f being PartFunc of [:X1,X2:],ExtREAL st E = dom f & f is nonnegative & f is E -measurable & A misses B holds
( Integral1 (M1,(f | (A \/ B))) = (Integral1 (M1,(f | A))) + (Integral1 (M1,(f | B))) & Integral2 (M2,(f | (A \/ B))) = (Integral2 (M2,(f | A))) + (Integral2 (M2,(f | B))) )
let M1 be sigma_Measure of S1; for M2 being sigma_Measure of S2
for E, A, B being Element of sigma (measurable_rectangles (S1,S2))
for f being PartFunc of [:X1,X2:],ExtREAL st E = dom f & f is nonnegative & f is E -measurable & A misses B holds
( Integral1 (M1,(f | (A \/ B))) = (Integral1 (M1,(f | A))) + (Integral1 (M1,(f | B))) & Integral2 (M2,(f | (A \/ B))) = (Integral2 (M2,(f | A))) + (Integral2 (M2,(f | B))) )
let M2 be sigma_Measure of S2; for E, A, B being Element of sigma (measurable_rectangles (S1,S2))
for f being PartFunc of [:X1,X2:],ExtREAL st E = dom f & f is nonnegative & f is E -measurable & A misses B holds
( Integral1 (M1,(f | (A \/ B))) = (Integral1 (M1,(f | A))) + (Integral1 (M1,(f | B))) & Integral2 (M2,(f | (A \/ B))) = (Integral2 (M2,(f | A))) + (Integral2 (M2,(f | B))) )
let E, A, B be Element of sigma (measurable_rectangles (S1,S2)); for f being PartFunc of [:X1,X2:],ExtREAL st E = dom f & f is nonnegative & f is E -measurable & A misses B holds
( Integral1 (M1,(f | (A \/ B))) = (Integral1 (M1,(f | A))) + (Integral1 (M1,(f | B))) & Integral2 (M2,(f | (A \/ B))) = (Integral2 (M2,(f | A))) + (Integral2 (M2,(f | B))) )
let f be PartFunc of [:X1,X2:],ExtREAL; ( E = dom f & f is nonnegative & f is E -measurable & A misses B implies ( Integral1 (M1,(f | (A \/ B))) = (Integral1 (M1,(f | A))) + (Integral1 (M1,(f | B))) & Integral2 (M2,(f | (A \/ B))) = (Integral2 (M2,(f | A))) + (Integral2 (M2,(f | B))) ) )
assume that
A1:
E = dom f
and
A2:
f is nonnegative
and
A3:
f is E -measurable
and
A4:
A misses B
; ( Integral1 (M1,(f | (A \/ B))) = (Integral1 (M1,(f | A))) + (Integral1 (M1,(f | B))) & Integral2 (M2,(f | (A \/ B))) = (Integral2 (M2,(f | A))) + (Integral2 (M2,(f | B))) )
Integral1 (M1,(f | A)) is V112()
by A1, A2, A3, Th66;
then reconsider IA = Integral1 (M1,(f | A)) as V120() Function of X2,ExtREAL ;
Integral1 (M1,(f | B)) is V112()
by A1, A2, A3, Th66;
then reconsider IB = Integral1 (M1,(f | B)) as V120() Function of X2,ExtREAL ;
now for y being Element of X2 holds (Integral1 (M1,(f | (A \/ B)))) . y = (IA + IB) . ylet y be
Element of
X2;
(Integral1 (M1,(f | (A \/ B)))) . y = (IA + IB) . yA5:
(
Y-section (
A,
y)
= Measurable-Y-section (
A,
y) &
Y-section (
B,
y)
= Measurable-Y-section (
B,
y) &
Y-section (
(A \/ B),
y)
= Measurable-Y-section (
(A \/ B),
y) )
by MEASUR11:def 7;
A6:
dom (ProjPMap2 (f,y)) =
Y-section (
E,
y)
by A1, Def4
.=
Measurable-Y-section (
E,
y)
by MEASUR11:def 7
;
A7:
ProjPMap2 (
f,
y) is
Measurable-Y-section (
E,
y)
-measurable
by A1, A3, Th47;
A /\ B = {} [:X1,X2:]
by A4;
then
Y-section (
(A /\ B),
y)
= {}
by MEASUR11:24;
then A8:
Measurable-Y-section (
A,
y)
misses Measurable-Y-section (
B,
y)
by A5, MEASUR11:27;
(
ProjPMap2 (
(f | A),
y)
= (ProjPMap2 (f,y)) | (Y-section (A,y)) &
ProjPMap2 (
(f | B),
y)
= (ProjPMap2 (f,y)) | (Y-section (B,y)) )
by Th34;
then A9:
(
ProjPMap2 (
(f | A),
y)
= (ProjPMap2 (f,y)) | (Measurable-Y-section (A,y)) &
ProjPMap2 (
(f | B),
y)
= (ProjPMap2 (f,y)) | (Measurable-Y-section (B,y)) )
by MEASUR11:def 7;
A10:
(Measurable-Y-section (A,y)) \/ (Measurable-Y-section (B,y)) = Measurable-Y-section (
(A \/ B),
y)
by A5, MEASUR11:26;
(IA + IB) . y =
((Integral1 (M1,(f | A))) . y) + ((Integral1 (M1,(f | B))) . y)
by DBLSEQ_3:7
.=
(Integral (M1,(ProjPMap2 ((f | A),y)))) + ((Integral1 (M1,(f | B))) . y)
by Def7
.=
(Integral (M1,(ProjPMap2 ((f | A),y)))) + (Integral (M1,(ProjPMap2 ((f | B),y))))
by Def7
.=
Integral (
M1,
((ProjPMap2 (f,y)) | (Measurable-Y-section ((A \/ B),y))))
by A2, A6, A7, A8, A9, A10, Th32, MESFUNC5:91
.=
Integral (
M1,
((ProjPMap2 (f,y)) | (Y-section ((A \/ B),y))))
by MEASUR11:def 7
.=
Integral (
M1,
(ProjPMap2 ((f | (A \/ B)),y)))
by Th34
;
hence
(Integral1 (M1,(f | (A \/ B)))) . y = (IA + IB) . y
by Def7;
verum end;
hence
Integral1 (M1,(f | (A \/ B))) = (Integral1 (M1,(f | A))) + (Integral1 (M1,(f | B)))
by FUNCT_2:def 8; Integral2 (M2,(f | (A \/ B))) = (Integral2 (M2,(f | A))) + (Integral2 (M2,(f | B)))
Integral2 (M2,(f | A)) is V112()
by A1, A2, A3, Th66;
then reconsider JA = Integral2 (M2,(f | A)) as V120() Function of X1,ExtREAL ;
Integral2 (M2,(f | B)) is V112()
by A1, A2, A3, Th66;
then reconsider JB = Integral2 (M2,(f | B)) as V120() Function of X1,ExtREAL ;
now for x being Element of X1 holds (Integral2 (M2,(f | (A \/ B)))) . x = (JA + JB) . xlet x be
Element of
X1;
(Integral2 (M2,(f | (A \/ B)))) . x = (JA + JB) . xA11:
(
X-section (
A,
x)
= Measurable-X-section (
A,
x) &
X-section (
B,
x)
= Measurable-X-section (
B,
x) &
X-section (
(A \/ B),
x)
= Measurable-X-section (
(A \/ B),
x) )
by MEASUR11:def 6;
A12:
dom (ProjPMap1 (f,x)) =
X-section (
E,
x)
by A1, Def3
.=
Measurable-X-section (
E,
x)
by MEASUR11:def 6
;
A13:
ProjPMap1 (
f,
x) is
Measurable-X-section (
E,
x)
-measurable
by A1, A3, Th47;
A /\ B = {} [:X1,X2:]
by A4;
then
X-section (
(A /\ B),
x)
= {}
by MEASUR11:24;
then A14:
Measurable-X-section (
A,
x)
misses Measurable-X-section (
B,
x)
by A11, MEASUR11:27;
(
ProjPMap1 (
(f | A),
x)
= (ProjPMap1 (f,x)) | (X-section (A,x)) &
ProjPMap1 (
(f | B),
x)
= (ProjPMap1 (f,x)) | (X-section (B,x)) )
by Th34;
then A15:
(
ProjPMap1 (
(f | A),
x)
= (ProjPMap1 (f,x)) | (Measurable-X-section (A,x)) &
ProjPMap1 (
(f | B),
x)
= (ProjPMap1 (f,x)) | (Measurable-X-section (B,x)) )
by MEASUR11:def 6;
A16:
(Measurable-X-section (A,x)) \/ (Measurable-X-section (B,x)) = Measurable-X-section (
(A \/ B),
x)
by A11, MEASUR11:26;
(JA + JB) . x =
((Integral2 (M2,(f | A))) . x) + ((Integral2 (M2,(f | B))) . x)
by DBLSEQ_3:7
.=
(Integral (M2,(ProjPMap1 ((f | A),x)))) + ((Integral2 (M2,(f | B))) . x)
by Def8
.=
(Integral (M2,(ProjPMap1 ((f | A),x)))) + (Integral (M2,(ProjPMap1 ((f | B),x))))
by Def8
.=
Integral (
M2,
((ProjPMap1 (f,x)) | (Measurable-X-section ((A \/ B),x))))
by A2, A12, A13, A14, A15, A16, Th32, MESFUNC5:91
.=
Integral (
M2,
((ProjPMap1 (f,x)) | (X-section ((A \/ B),x))))
by MEASUR11:def 6
.=
Integral (
M2,
(ProjPMap1 ((f | (A \/ B)),x)))
by Th34
;
hence
(Integral2 (M2,(f | (A \/ B)))) . x = (JA + JB) . x
by Def8;
verum end;
hence
Integral2 (M2,(f | (A \/ B))) = (Integral2 (M2,(f | A))) + (Integral2 (M2,(f | B)))
by FUNCT_2:def 8; verum