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

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

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

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

end;

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

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

end;

end;