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 M2 is sigma_finite & E1 misses E2 holds
Integral (M1,(Y-vol ((E1 \/ E2),M2))) = (Integral (M1,(Y-vol (E1,M2)))) + (Integral (M1,(Y-vol (E2,M2))))
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 M2 is sigma_finite & E1 misses E2 holds
Integral (M1,(Y-vol ((E1 \/ E2),M2))) = (Integral (M1,(Y-vol (E1,M2)))) + (Integral (M1,(Y-vol (E2,M2))))
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 M2 is sigma_finite & E1 misses E2 holds
Integral (M1,(Y-vol ((E1 \/ E2),M2))) = (Integral (M1,(Y-vol (E1,M2)))) + (Integral (M1,(Y-vol (E2,M2))))
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 M2 is sigma_finite & E1 misses E2 holds
Integral (M1,(Y-vol ((E1 \/ E2),M2))) = (Integral (M1,(Y-vol (E1,M2)))) + (Integral (M1,(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
Integral (M1,(Y-vol ((E1 \/ E2),M2))) = (Integral (M1,(Y-vol (E1,M2)))) + (Integral (M1,(Y-vol (E2,M2))))
let E1, E2 be Element of sigma (measurable_rectangles (S1,S2)); :: thesis: ( M2 is sigma_finite & E1 misses E2 implies Integral (M1,(Y-vol ((E1 \/ E2),M2))) = (Integral (M1,(Y-vol (E1,M2)))) + (Integral (M1,(Y-vol (E2,M2)))) )
assume that
A1: M2 is sigma_finite and
A2: E1 misses E2 ; :: thesis: Integral (M1,(Y-vol ((E1 \/ E2),M2))) = (Integral (M1,(Y-vol (E1,M2)))) + (Integral (M1,(Y-vol (E2,M2))))
reconsider XX1 = X1 as Element of S1 by MEASURE1:7;
a3: Y-vol ((E1 \/ E2),M2) = (Y-vol (E1,M2)) + (Y-vol (E2,M2)) by A1, A2, Th92;
A3: ( dom (Y-vol (E1,M2)) = XX1 & Y-vol (E1,M2) is XX1 -measurable ) by A1, DefYvol, FUNCT_2:def 1;
A4: ( dom (Y-vol (E2,M2)) = XX1 & Y-vol (E2,M2) is XX1 -measurable ) by A1, DefYvol, FUNCT_2:def 1;
A5: ( dom (Y-vol ((E1 \/ E2),M2)) = XX1 & Y-vol ((E1 \/ E2),M2) is XX1 -measurable ) by A1, DefYvol, FUNCT_2:def 1;
reconsider Y1 = Y-vol (E1,M2) as PartFunc of X1,ExtREAL ;
reconsider Y2 = Y-vol (E2,M2) as PartFunc of X1,ExtREAL ;
ex Z being Element of S1 st
( Z = dom ((Y-vol (E1,M2)) + (Y-vol (E2,M2))) & integral+ (M1,((Y-vol (E1,M2)) + (Y-vol (E2,M2)))) = (integral+ (M1,(Y1 | Z))) + (integral+ (M1,(Y2 | Z))) ) by A3, A4, MESFUNC5:78;
then Integral (M1,(Y-vol ((E1 \/ E2),M2))) = (integral+ (M1,(Y-vol (E1,M2)))) + (integral+ (M1,(Y-vol (E2,M2)))) by a3, A5, MESFUNC5:88
.= (Integral (M1,(Y-vol (E1,M2)))) + (integral+ (M1,(Y-vol (E2,M2)))) by A3, MESFUNC5:88 ;
hence Integral (M1,(Y-vol ((E1 \/ E2),M2))) = (Integral (M1,(Y-vol (E1,M2)))) + (Integral (M1,(Y-vol (E2,M2)))) by A4, MESFUNC5:88; :: thesis: verum