for X being set
for F1, F2 being disjoint_valued FinSequence of X st union (rng F1) misses union (rng F2) holds
F1 ^ F2 is disjoint_valued FinSequence of X