theorem Th16: :: AFINSQ_1:18

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