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))) & (Seq q1) ^ (Seq q2) = Seq ss )