theorem Th46: :: FINSEQ_4:46

for p being FinSequence
for x being object st x in rng p & p is one-to-one holds
not x in rng (p |-- x)