theorem :: AFINSQ_1:24

for p, q being XFinSequence holds rng p c= rng (p ^ q)