theorem Th34: :: FINSEQ_5:34

for n being Nat
for D being non empty set
for f being FinSequence of D st f is one-to-one holds
rng (f | n) misses rng (f /^ n)