for n being Nat
for f being FinSequence holds rng (f /^ n) c= rng f