theorem Th28: :: FINSEQ_1:28

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