theorem Th77: :: AFINSQ_1:80

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