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 E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite & E1 misses E2 holds
X-vol ((E1 \/ E2),M1) = (X-vol (E1,M1)) + (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 E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite & E1 misses E2 holds
X-vol ((E1 \/ E2),M1) = (X-vol (E1,M1)) + (X-vol (E2,M1))
let S2 be SigmaField of X2; :: thesis: for M1 being sigma_Measure of S1
for E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite & E1 misses E2 holds
X-vol ((E1 \/ E2),M1) = (X-vol (E1,M1)) + (X-vol (E2,M1))
let M1 be sigma_Measure of S1; :: thesis: for E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite & E1 misses E2 holds
X-vol ((E1 \/ E2),M1) = (X-vol (E1,M1)) + (X-vol (E2,M1))
let E1, E2 be Element of sigma (measurable_rectangles (S1,S2)); :: thesis: ( M1 is sigma_finite & E1 misses E2 implies X-vol ((E1 \/ E2),M1) = (X-vol (E1,M1)) + (X-vol (E2,M1)) )
assume that
A1: M1 is sigma_finite and
A2: E1 misses E2 ; :: thesis: X-vol ((E1 \/ E2),M1) = (X-vol (E1,M1)) + (X-vol (E2,M1))
A3: ( dom (X-vol ((E1 \/ E2),M1)) = X2 & dom (X-vol (E1,M1)) = X2 & dom (X-vol (E2,M1)) = X2 ) by FUNCT_2:def 1;
then A4: dom ((X-vol (E1,M1)) + (X-vol (E2,M1))) = X2 /\ X2 by MESFUNC5:22;
for x being Element of X2 st x in dom (X-vol ((E1 \/ E2),M1)) holds
(X-vol ((E1 \/ E2),M1)) . x = ((X-vol (E1,M1)) + (X-vol (E2,M1))) . x

proof

let x be Element of X2; :: thesis: ( x in dom (X-vol ((E1 \/ E2),M1)) implies (X-vol ((E1 \/ E2),M1)) . x = ((X-vol (E1,M1)) + (X-vol (E2,M1))) . x )
assume x in dom (X-vol ((E1 \/ E2),M1)) ; :: thesis: (X-vol ((E1 \/ E2),M1)) . x = ((X-vol (E1,M1)) + (X-vol (E2,M1))) . x
A6: ( (X-vol ((E1 \/ E2),M1)) . x = M1 . (Measurable-Y-section ((E1 \/ E2),x)) & (X-vol (E1,M1)) . x = M1 . (Measurable-Y-section (E1,x)) & (X-vol (E2,M1)) . x = M1 . (Measurable-Y-section (E2,x)) ) by A1, DefXvol;
Measurable-Y-section ((E1 \/ E2),x) = (Measurable-Y-section (E1,x)) \/ (Measurable-Y-section (E2,x)) by Th20;
then (X-vol ((E1 \/ E2),M1)) . x = ((X-vol (E1,M1)) . x) + ((X-vol (E2,M1)) . x) by A6, A2, Th29, MEASURE1:30;
hence (X-vol ((E1 \/ E2),M1)) . x = ((X-vol (E1,M1)) + (X-vol (E2,M1))) . x by A4, MESFUNC1:def 3; :: thesis: verum

end;

hence X-vol ((E1 \/ E2),M1) = (X-vol (E1,M1)) + (X-vol (E2,M1)) by A4, A3, PARTFUN1:5; :: thesis: verum