theorem :: AFINSQ_2:17

for k being Nat
for p being XFinSequence st len p <= k holds
mid (p,1,k) = p