theorem Th5: :: PENCIL_2:5

for p, q being FinSequence
for k being Element of NAT st (len p) + 1 <= k holds
(p ^ q) . k = q . (k - (len p))