let i1, i2 be Nat; :: thesis:
let f1 be FinSequence; :: thesis:
set k1 = i1;
set k2 = i2;

now :: thesis:

per cases ;

case A1: i1 <= i2 ; :: thesis:

then A2: mid (f1,i1,i2) = (f1 /^ (i1 -' 1)) | ((i2 -' i1) + 1) by FINSEQ_6:def 3;

now :: thesis:

per cases by A1, XXREAL_0:1;

case i1 < i2 ; :: thesis:

then mid (f1,i2,i1) = Rev (mid (f1,i1,i2)) by A2, FINSEQ_6:def 3;
hence mid (f1,i1,i2) = Rev (mid (f1,i2,i1)) ; :: thesis:

end;

case A3: i1 = i2 ; :: thesis:

A4: ( i1 = 0 or 0 + 1 <= i1 ) by NAT_1:13;

now :: thesis:

per cases by A4;

case i1 = 0 ; :: thesis:

then A5: mid (f1,i1,i2) = f1 | 1 by A3, Th16;

now :: thesis:

per cases ;

case len f1 = 0 ; :: thesis:

then f1 = {} ;
then f1 | 1 = {} ;
hence mid (f1,i1,i2) = Rev (mid (f1,i2,i1)) by A3, A5; :: thesis:

end;

case len f1 <> 0 ; :: thesis:

then f1 <> {} ;
then f1 | 1 = <*(f1 . 1)*> by FINSEQ_5:20;
hence mid (f1,i1,i2) = Rev (mid (f1,i2,i1)) by A3, A5, FINSEQ_5:60; :: thesis:

end;

end;

end;

hence mid (f1,i1,i2) = Rev (mid (f1,i2,i1)) ; :: thesis:

end;

case ( 1 <= i1 & i1 <= len f1 ) ; :: thesis:

then i1 in dom f1 by FINSEQ_3:25;
then mid (f1,i1,i1) = <*(f1 . i1)*> by Th15;
hence mid (f1,i1,i2) = Rev (mid (f1,i2,i1)) by A3, FINSEQ_5:60; :: thesis:

end;

case len f1 < i1 ; :: thesis:

then mid (f1,i1,i1) = {} by Th17;
hence mid (f1,i1,i2) = Rev (mid (f1,i2,i1)) by A3; :: thesis:

end;

end;

end;

hence mid (f1,i1,i2) = Rev (mid (f1,i2,i1)) ; :: thesis:

end;

end;

end;

hence mid (f1,i1,i2) = Rev (mid (f1,i2,i1)) ; :: thesis:

end;

case A6: i1 > i2 ; :: thesis:

then mid (f1,i1,i2) = Rev ((f1 /^ (i2 -' 1)) | ((i1 -' i2) + 1)) by FINSEQ_6:def 3;
hence mid (f1,i1,i2) = Rev (mid (f1,i2,i1)) by A6, FINSEQ_6:def 3; :: thesis:

end;

end;

end;

hence mid (f1,i1,i2) = Rev (mid (f1,i2,i1)) ; :: thesis: