let f be special FinSequence of (TOP-REAL 2); :: thesis: for i, j being Element of NAT holds mid f,i,j is special
let i, j be Element of 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 JORDAN3:def 1;
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 JORDAN3:def 1;
then Rev (mid f,i,j) is special by JORDAN4:30;
then Rev (Rev (mid f,i,j)) is special by SPPOL_2:42;
hence mid f,i,j is special by FINSEQ_6:29; :: thesis: verum

end;

end;