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