theorem Th24: :: FINSEQ_1:24

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