for F being disjoint_valued FinSequence of Family_of_Intervals st Union F in Family_of_Intervals holds
pre-Meas . (Union F) = Sum (pre-Meas * F)