for p1, p2 being FinSequence holds dom (p1 \/ (Shift (p2,(len p1)))) = Seg ((len p1) + (len p2))