theorem Th21: :: AFINSQ_1:23

for k being Nat
for p, q being XFinSequence st k in dom q holds
(len p) + k in dom (p ^ q)