theorem Th33: :: FINSEQ_4:33

for p being FinSequence
for x being object
for n being Nat st x in rng p & n = (x .. p) - 1 holds
p | (Seg n) = p -| x