theorem Th9: :: AFINSQ_2:9

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