for f1, f2 being disjoint_valued FinSequence ex f being disjoint_valued FinSequence st
( (Union f1) /\ (Union f2) = Union f & dom f = Seg ((len f1) * (len f2)) & ( for i being Nat st i in dom f holds
f . i = (f1 . (((i -' 1) div (len f2)) + 1)) /\ (f2 . (((i -' 1) mod (len f2)) + 1)) ) )