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