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