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