theorem :: MEASURE9:40

for X being set
for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X
for P being pre-Measure of S
for F1, F2 being disjoint_valued FinSequence of S st Union F1 in S & Union F1 = Union F2 holds
P . (Union F1) = P . (Union F2) ;