let D be non empty set ; :: thesis: for f1 being FinSequence of D
for i1, i2 being Nat holds mid (f1,i1,i2) = Rev (mid (f1,i2,i1))
let f1 be FinSequence of D; :: thesis: for i1, i2 being Nat holds mid (f1,i1,i2) = Rev (mid (f1,i2,i1))
let k1, k2 be Nat; :: thesis: mid (f1,k1,k2) = Rev (mid (f1,k2,k1))

now :: thesis: ( ( k1 <= k2 & mid (f1,k1,k2) = Rev (mid (f1,k2,k1)) ) or ( k1 > k2 & mid (f1,k1,k2) = Rev (mid (f1,k2,k1)) ) )

per cases ( k1 <= k2 or k1 > k2 ) ;

case A1: k1 <= k2 ; :: thesis: mid (f1,k1,k2) = Rev (mid (f1,k2,k1))

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

now :: thesis: ( ( k1 < k2 & mid (f1,k1,k2) = Rev (mid (f1,k2,k1)) ) or ( k1 = k2 & mid (f1,k1,k2) = Rev (mid (f1,k2,k1)) ) )

per cases ( k1 < k2 or k1 = k2 ) by A1, XXREAL_0:1;

case k1 < k2 ; :: thesis: mid (f1,k1,k2) = Rev (mid (f1,k2,k1))

then mid (f1,k2,k1) = Rev (mid (f1,k1,k2)) by A2, FINSEQ_6:def 3;
hence mid (f1,k1,k2) = Rev (mid (f1,k2,k1)) ; :: thesis: verum

end;

case A3: k1 = k2 ; :: thesis: mid (f1,k1,k2) = Rev (mid (f1,k2,k1))

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

now :: thesis: ( ( k1 = 0 & mid (f1,k1,k2) = Rev (mid (f1,k2,k1)) ) or ( 1 <= k1 & k1 <= len f1 & mid (f1,k1,k2) = Rev (mid (f1,k2,k1)) ) or ( len f1 < k1 & mid (f1,k1,k2) = Rev (mid (f1,k2,k1)) ) )

per cases ( k1 = 0 or ( 1 <= k1 & k1 <= len f1 ) or len f1 < k1 ) by A4;

case k1 = 0 ; :: thesis: mid (f1,k1,k2) = Rev (mid (f1,k2,k1))

then A5: mid (f1,k1,k2) = f1 | 1 by A3, Lm4;

now :: thesis: ( ( len f1 = 0 & mid (f1,k1,k2) = Rev (mid (f1,k2,k1)) ) or ( len f1 <> 0 & mid (f1,k1,k2) = Rev (mid (f1,k2,k1)) ) )

per cases ( len f1 = 0 or len f1 <> 0 ) ;

case len f1 = 0 ; :: thesis: mid (f1,k1,k2) = Rev (mid (f1,k2,k1))

then f1 = <*> D ;
then f1 | 1 = <*> D by Lm2;
hence mid (f1,k1,k2) = Rev (mid (f1,k2,k1)) by A3, A5; :: thesis: verum

end;

case len f1 <> 0 ; :: thesis: mid (f1,k1,k2) = Rev (mid (f1,k2,k1))

then f1 <> <*> D ;
then f1 | 1 = <*(f1 . 1)*> by FINSEQ_5:20;
hence mid (f1,k1,k2) = Rev (mid (f1,k2,k1)) by A3, A5, FINSEQ_5:60; :: thesis: verum

end;

end;

end;

hence mid (f1,k1,k2) = Rev (mid (f1,k2,k1)) ; :: thesis: verum

end;

case ( 1 <= k1 & k1 <= len f1 ) ; :: thesis: mid (f1,k1,k2) = Rev (mid (f1,k2,k1))

then mid (f1,k1,k1) = <*(f1 /. k1)*> by Lm3;
hence mid (f1,k1,k2) = Rev (mid (f1,k2,k1)) by A3, FINSEQ_5:60; :: thesis: verum

end;

case len f1 < k1 ; :: thesis: mid (f1,k1,k2) = Rev (mid (f1,k2,k1))

then mid (f1,k1,k1) = <*> D by Lm5;
hence mid (f1,k1,k2) = Rev (mid (f1,k2,k1)) by A3; :: thesis: verum

end;

end;

end;

hence mid (f1,k1,k2) = Rev (mid (f1,k2,k1)) ; :: thesis: verum

end;

end;

end;

hence mid (f1,k1,k2) = Rev (mid (f1,k2,k1)) ; :: thesis: verum

end;

case A6: k1 > k2 ; :: thesis: mid (f1,k1,k2) = Rev (mid (f1,k2,k1))

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

end;

end;

end;

hence mid (f1,k1,k2) = Rev (mid (f1,k2,k1)) ; :: thesis: verum