theorem :: AFINSQ_2:18

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