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