theorem Th17: :: CHORD:17

for p, q being FinSequence
for x being set st p = <*x*> ^ q holds
for n being non zero Nat holds p .followSet (n + 1) = q .followSet n