for n being Nat
for p being XFinSequence holds rng (p /^ n) c= rng p