theorem :: AFINSQ_1:51

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