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

now

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 Def1;

now

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, Def1;
hence mid f1,k1,k2 = Rev (mid f1,k2,k1) by FINSEQ_6:29; :: 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

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

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:23;
hence mid f1,k1,k2 = Rev (mid f1,k2,k1) by A3, A5, FINSEQ_5:63; :: 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:63; :: 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 Def1;
hence mid f1,k1,k2 = Rev (mid f1,k2,k1) by A6, Def1; :: thesis: verum

end;

end;

end;

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