for p being XFinSequence
for k1, k2 being Nat st k1 > k2 holds
mid (p,k1,k2) = {}