theorem Th37: :: FINSEQ_4:37

for p being FinSequence
for x being object st x in rng p holds
not x in rng (p -| x)