for F being disjoint_valued FinSequence
for n, m being Nat st n < m holds
union (rng (F | n)) misses F . m