theorem Th35: :: FINSEQ_4:35

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