theorem Th14: :: FINSEQ_6:140

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