theorem Th78: :: AFINSQ_1:81

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