for f being special FinSequence of (TOP-REAL 2)
for i, j being Nat holds mid (f,i,j) is special