theorem :: AFINSQ_2:87

for D being set
for p being one-to-one XFinSequence of D
for n being Nat holds rng (p | n) misses rng (p /^ n)