let X1, X2 be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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)); :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum