for i being Nat
for p1 being FinSequence
for p2 being FinSubsequence st len p1 <= i holds
dom p1 misses dom (Shift (p2,i))