theorem :: MEASUR10:25

for X1, X2 being set
for S1 being Field_Subset of X1
for S2 being Field_Subset of X2
for m1 being Measure of S1
for m2 being Measure of S2
for E1, E2 being Element of measurable_rectangles (S1,S2) st E1 misses E2 & E1 \/ E2 in measurable_rectangles (S1,S2) holds
(product-pre-Measure (m1,m2)) . (E1 \/ E2) = ((product-pre-Measure (m1,m2)) . E1) + ((product-pre-Measure (m1,m2)) . E2)