theorem Th11: :: AFINSQ_2:11

for i being Nat
for p, q being XFinSequence holds (p ^ q) /^ ((len p) + i) = q /^ i