theorem :: AFINSQ_1:59

for k, n being Nat
for p, q being XFinSequence st n = (dom p) + k holds
(p ^ q) | n = p ^ (q | k)