for k being Nat
for E being non empty set
for p, q being FinSequence of E st k in dom q holds
(p ^ q) /. ((len p) + k) = q /. k