for f, g being FinSequence holds dom (f ^ g) = (dom f) \/ (seq ((len f),(len g)))