theorem Th34: :: FINSEQ_4:34

for p being FinSequence
for x being object st x in rng p holds
len (p -| x) = (x .. p) - 1