:: deftheorem defines mid AFINSQ_2:def 3 :
for p being XFinSequence
for k1, k2 being Nat holds mid (p,k1,k2) = (p | k2) /^ (k1 -' 1);