:: deftheorem defines .followSet CHORD:def 1 :
for p being FinSequence
for n being Nat holds p .followSet n = rng ((n,(len p)) -cut p);