theorem Th34: :: FINSEQ_5:34

for n being Nat
for f being FinSequence st f is one-to-one holds
rng (f | n) misses rng (f /^ n)