let f be unfolded FinSequence of (TOP-REAL 2); :: thesis: for i, j being Nat holds mid (f,i,j) is unfolded
let i, j be 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 FINSEQ_6:196;
then Rev (Rev (mid (f,i,j))) is unfolded by SPPOL_2:28;
hence mid (f,i,j) is unfolded ; :: thesis: verum

end;

end;