theorem Th15: :: FINSEQ_6:141

for p, q being FinSequence
for k being Nat st 1 <= k & k < len q holds
(p ^' q) . ((len p) + k) = q . (k + 1)