theorem :: AFINSQ_1:83

for X being set
for p, q being XFinSequence
for n being Nat st Shift ((p ^ q),n) c= X holds
Shift (q,(n + (card p))) c= X