theorem Th16: :: AFINSQ_2:16

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