theorem :: CALCUL_2:9

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