for k being Nat
for p being XFinSequence holds mid (p,1,k) = p | k