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