theorem Th17: :: AFINSQ_1:19

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