theorem :: AFINSQ_1:25

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