for F being disjoint_valued FinSequence of Family_of_Intervals st Union F in Family_of_Intervals holds
ex G being disjoint_valued FinSequence of Family_of_Intervals st
( F,G are_fiberwise_equipotent & ( for n being Nat st n in dom G holds
( Union (G | n) in Family_of_Intervals & pre-Meas . (Union (G | n)) = Sum (pre-Meas * (G | n)) ) ) )