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 E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite & E1 misses E2 holds
Integral (M2,(X-vol ((E1 \/ E2),M1))) = (Integral (M2,(X-vol (E1,M1)))) + (Integral (M2,(X-vol (E2,M1))))
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 E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite & E1 misses E2 holds
Integral (M2,(X-vol ((E1 \/ E2),M1))) = (Integral (M2,(X-vol (E1,M1)))) + (Integral (M2,(X-vol (E2,M1))))
let S2 be SigmaField of X2; for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite & E1 misses E2 holds
Integral (M2,(X-vol ((E1 \/ E2),M1))) = (Integral (M2,(X-vol (E1,M1)))) + (Integral (M2,(X-vol (E2,M1))))
let M1 be sigma_Measure of S1; for M2 being sigma_Measure of S2
for E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite & E1 misses E2 holds
Integral (M2,(X-vol ((E1 \/ E2),M1))) = (Integral (M2,(X-vol (E1,M1)))) + (Integral (M2,(X-vol (E2,M1))))
let M2 be sigma_Measure of S2; for E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite & E1 misses E2 holds
Integral (M2,(X-vol ((E1 \/ E2),M1))) = (Integral (M2,(X-vol (E1,M1)))) + (Integral (M2,(X-vol (E2,M1))))
let E1, E2 be Element of sigma (measurable_rectangles (S1,S2)); ( M1 is sigma_finite & E1 misses E2 implies Integral (M2,(X-vol ((E1 \/ E2),M1))) = (Integral (M2,(X-vol (E1,M1)))) + (Integral (M2,(X-vol (E2,M1)))) )
assume that
A1:
M1 is sigma_finite
and
A2:
E1 misses E2
; Integral (M2,(X-vol ((E1 \/ E2),M1))) = (Integral (M2,(X-vol (E1,M1)))) + (Integral (M2,(X-vol (E2,M1))))
reconsider XX2 = X2 as Element of S2 by MEASURE1:7;
a3:
X-vol ((E1 \/ E2),M1) = (X-vol (E1,M1)) + (X-vol (E2,M1))
by A1, A2, Th93;
A3:
( dom (X-vol (E1,M1)) = XX2 & X-vol (E1,M1) is XX2 -measurable )
by A1, DefXvol, FUNCT_2:def 1;
A4:
( dom (X-vol (E2,M1)) = XX2 & X-vol (E2,M1) is XX2 -measurable )
by A1, DefXvol, FUNCT_2:def 1;
A5:
( dom (X-vol ((E1 \/ E2),M1)) = XX2 & X-vol ((E1 \/ E2),M1) is XX2 -measurable )
by A1, DefXvol, FUNCT_2:def 1;
reconsider V1 = X-vol (E1,M1) as PartFunc of X2,ExtREAL ;
reconsider V2 = X-vol (E2,M1) as PartFunc of X2,ExtREAL ;
ex Z being Element of S2 st
( Z = dom ((X-vol (E1,M1)) + (X-vol (E2,M1))) & integral+ (M2,((X-vol (E1,M1)) + (X-vol (E2,M1)))) = (integral+ (M2,(V1 | Z))) + (integral+ (M2,(V2 | Z))) )
by A3, A4, MESFUNC5:78;
then Integral (M2,(X-vol ((E1 \/ E2),M1))) =
(integral+ (M2,(X-vol (E1,M1)))) + (integral+ (M2,(X-vol (E2,M1))))
by a3, A5, MESFUNC5:88
.=
(Integral (M2,(X-vol (E1,M1)))) + (integral+ (M2,(X-vol (E2,M1))))
by A3, MESFUNC5:88
;
hence
Integral (M2,(X-vol ((E1 \/ E2),M1))) = (Integral (M2,(X-vol (E1,M1)))) + (Integral (M2,(X-vol (E2,M1))))
by A4, MESFUNC5:88; verum