theorem Th17: :: POLYFORM:19

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