for p1, p2 being FinSequence
for q1, q2 being FinSubsequence st q1 c= p1 & q2 c= p2 holds
ex ss being FinSubsequence st
( ss = q1 \/ (Shift (q2,(len p1))) & dom (Seq ss) = Seg ((len (Seq q1)) + (len (Seq q2))) & Seq ss = (Seq q1) \/ (Shift ((Seq q2),(len (Seq q1)))) )