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 JORDAN3:def 1;
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 JORDAN3:def 1;
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;