for p being FinSequence
for A being set holds len (p - A) <= len p