let X1, X2 be non empty set ; :: thesis: for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M2 being sigma_Measure of S2
for E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st M2 is sigma_finite & E1 misses E2 holds
Y-vol ((E1 \/ E2),M2) = (Y-vol (E1,M2)) + (Y-vol (E2,M2))
let S1 be SigmaField of X1; :: thesis: for S2 being SigmaField of X2
for M2 being sigma_Measure of S2
for E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st M2 is sigma_finite & E1 misses E2 holds
Y-vol ((E1 \/ E2),M2) = (Y-vol (E1,M2)) + (Y-vol (E2,M2))
let S2 be SigmaField of X2; :: thesis: for M2 being sigma_Measure of S2
for E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st M2 is sigma_finite & E1 misses E2 holds
Y-vol ((E1 \/ E2),M2) = (Y-vol (E1,M2)) + (Y-vol (E2,M2))
let M2 be sigma_Measure of S2; :: thesis: for E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st M2 is sigma_finite & E1 misses E2 holds
Y-vol ((E1 \/ E2),M2) = (Y-vol (E1,M2)) + (Y-vol (E2,M2))
let E1, E2 be Element of sigma (measurable_rectangles (S1,S2)); :: thesis: ( M2 is sigma_finite & E1 misses E2 implies Y-vol ((E1 \/ E2),M2) = (Y-vol (E1,M2)) + (Y-vol (E2,M2)) )
assume that
A1: M2 is sigma_finite and
A2: E1 misses E2 ; :: thesis: Y-vol ((E1 \/ E2),M2) = (Y-vol (E1,M2)) + (Y-vol (E2,M2))
A3: ( dom (Y-vol ((E1 \/ E2),M2)) = X1 & dom (Y-vol (E1,M2)) = X1 & dom (Y-vol (E2,M2)) = X1 ) by FUNCT_2:def 1;
then A4: dom ((Y-vol (E1,M2)) + (Y-vol (E2,M2))) = X1 /\ X1 by MESFUNC5:22;
for x being Element of X1 st x in dom (Y-vol ((E1 \/ E2),M2)) holds
(Y-vol ((E1 \/ E2),M2)) . x = ((Y-vol (E1,M2)) + (Y-vol (E2,M2))) . x

proof

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

end;

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