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