theorem Th23: :: FINSEQ_1:23

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