let f be special FinSequence of (TOP-REAL 2); :: thesis: for i, j being Nat holds mid (f,i,j) is special
let i, j be Nat; :: thesis: mid (f,i,j) is special

per cases ( i <= j or j < i ) ;

suppose i <= j ; :: thesis: mid (f,i,j) is special

then mid (f,i,j) = (f /^ (i -' 1)) | ((j -' i) + 1) by FINSEQ_6:def 3;
hence mid (f,i,j) is special ; :: thesis: verum

end;

suppose j < i ; :: thesis: mid (f,i,j) is special

then mid (f,j,i) = (f /^ (j -' 1)) | ((i -' j) + 1) by FINSEQ_6:def 3;
then Rev (mid (f,i,j)) is special by FINSEQ_6:196;
then Rev (Rev (mid (f,i,j))) is special by SPPOL_2:40;
hence mid (f,i,j) is special ; :: thesis: verum

end;

end;