let D be non empty set ; :: thesis: for f being FinSequence of D
for k1, k2 being Element of NAT st 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f holds
Rev (mid f,k1,k2) = mid (Rev f),(((len f) -' k2) + 1),(((len f) -' k1) + 1)
let f be FinSequence of D; :: thesis: for k1, k2 being Element of NAT st 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f holds
Rev (mid f,k1,k2) = mid (Rev f),(((len f) -' k2) + 1),(((len f) -' k1) + 1)
let k1, k2 be Element of NAT ; :: thesis: ( 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f implies Rev (mid f,k1,k2) = mid (Rev f),(((len f) -' k2) + 1),(((len f) -' k1) + 1) )
assume A1: ( 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f ) ; :: thesis: Rev (mid f,k1,k2) = mid (Rev f),(((len f) -' k2) + 1),(((len f) -' k1) + 1)

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

suppose A2: k1 <= k2 ; :: thesis: Rev (mid f,k1,k2) = mid (Rev f),(((len f) -' k2) + 1),(((len f) -' k1) + 1)

A3: (len f) -' k1 = (len f) - k1 by A1, XREAL_1:235;
A4: (len f) -' k2 = (len f) - k2 by A1, XREAL_1:235;
A5: ((len f) -' (k1 -' 1)) + (k1 -' 1) = ((len f) - (k1 -' 1)) + (k1 -' 1) by A1, NAT_D:50, XREAL_1:235
.= len f ;
A6: (len f) -' (k1 -' 1) = (len f) - (k1 -' 1) by A1, NAT_D:50, XREAL_1:235
.= (len f) - (k1 - 1) by A1, XREAL_1:235
.= ((len f) - k1) + 1
.= ((len f) -' k1) + 1 by A1, XREAL_1:235 ;
(len f) -' k1 >= (len f) -' k2 by A2, NAT_D:41;
then A7: ((len f) -' k1) + 1 >= ((len f) -' k2) + 1 by XREAL_1:8;
k2 - k1 <= (len f) - k1 by A1, XREAL_1:11;
then k2 -' k1 <= (len f) - k1 by A2, XREAL_1:235;
then k2 -' k1 <= (len f) -' k1 by A1, XREAL_1:235;
then (k2 -' k1) + 1 <= ((len f) -' k1) + 1 by XREAL_1:8;
then A8: ((len f) -' (k1 -' 1)) -' ((k2 -' k1) + 1) = (((len f) -' k1) + 1) - ((k2 -' k1) + 1) by A6, XREAL_1:235
.= (((len f) - k1) + 1) - ((k2 - k1) + 1) by A2, A3, XREAL_1:235
.= (((len f) + 1) - 1) - k2
.= (len f) -' k2 by A1, XREAL_1:235 ;
A9: (len f) -' k1 >= (len f) -' k2 by A2, NAT_D:41;
(len f) -' k1 <= ((len f) -' k1) + 1 by NAT_1:11;
then A10: ((len f) -' (k1 -' 1)) -' ((len f) -' k2) = (((len f) -' k1) + 1) - ((len f) -' k2) by A6, A9, XREAL_1:235, XXREAL_0:2
.= (((len f) - k1) + 1) - ((len f) - k2) by A1, A3, XREAL_1:235
.= (k2 - k1) + 1
.= (k2 -' k1) + 1 by A2, XREAL_1:235 ;
A11: ((len (f /^ (k1 -' 1))) -' ((k2 -' k1) + 1)) + ((k2 -' k1) + 1) = ((len f) -' k2) + ((k2 -' k1) + 1) by A8, RFINSEQ:42
.= ((len f) - k2) + ((k2 - k1) + 1) by A2, A4, XREAL_1:235
.= (len f) - (k1 - 1)
.= (len f) - (k1 -' 1) by A1, XREAL_1:235
.= (len f) -' (k1 -' 1) by A1, NAT_D:50, XREAL_1:235
.= len (f /^ (k1 -' 1)) by RFINSEQ:42 ;
A12: ((((len f) -' k1) + 1) -' (((len f) -' k2) + 1)) + 1 = ((((len f) -' k1) + 1) - (((len f) -' k2) + 1)) + 1 by A7, XREAL_1:235
.= ((((len f) - k1) + 1) - (((len f) - k2) + 1)) + 1 by A1, A3, XREAL_1:235
.= (k2 - k1) + 1
.= (k2 -' k1) + 1 by A2, XREAL_1:235 ;
(len f) -' k1 >= (len f) -' k2 by A2, NAT_D:41;
then ((len f) -' k1) + 1 >= ((len f) -' k2) + 1 by XREAL_1:8;
then mid (Rev f),(((len f) -' k2) + 1),(((len f) -' k1) + 1) = ((Rev f) /^ ((((len f) -' k2) + 1) -' 1)) | ((k2 -' k1) + 1) by A12, Def1
.= ((Rev f) /^ ((len f) -' k2)) | (((len f) -' (k1 -' 1)) -' ((len f) -' k2)) by A10, NAT_D:34
.= ((Rev f) | ((len f) -' (k1 -' 1))) /^ ((len f) -' k2) by FINSEQ_5:83
.= ((Rev f) | ((len f) -' (k1 -' 1))) /^ ((len (f /^ (k1 -' 1))) -' ((k2 -' k1) + 1)) by A8, RFINSEQ:42
.= (Rev (f /^ (k1 -' 1))) /^ ((len (f /^ (k1 -' 1))) -' ((k2 -' k1) + 1)) by A5, FINSEQ_6:90
.= Rev ((f /^ (k1 -' 1)) | ((k2 -' k1) + 1)) by A11, FINSEQ_6:91
.= Rev (mid f,k1,k2) by A2, Def1 ;
hence Rev (mid f,k1,k2) = mid (Rev f),(((len f) -' k2) + 1),(((len f) -' k1) + 1) ; :: thesis: verum

end;

suppose A13: k1 > k2 ; :: thesis: Rev (mid f,k1,k2) = mid (Rev f),(((len f) -' k2) + 1),(((len f) -' k1) + 1)

A14: (len f) -' k2 = (len f) - k2 by A1, XREAL_1:235;
A15: (len f) -' k1 = (len f) - k1 by A1, XREAL_1:235;
A16: ((len f) -' (k2 -' 1)) + (k2 -' 1) = ((len f) - (k2 -' 1)) + (k2 -' 1) by A1, NAT_D:50, XREAL_1:235
.= len f ;
A17: (len f) -' (k2 -' 1) = (len f) - (k2 -' 1) by A1, NAT_D:50, XREAL_1:235
.= (len f) - (k2 - 1) by A1, XREAL_1:235
.= ((len f) - k2) + 1
.= ((len f) -' k2) + 1 by A1, XREAL_1:235 ;
(len f) -' k2 >= (len f) -' k1 by A13, NAT_D:41;
then A18: ((len f) -' k2) + 1 >= ((len f) -' k1) + 1 by XREAL_1:8;
k1 - k2 <= (len f) - k2 by A1, XREAL_1:11;
then k1 -' k2 <= (len f) - k2 by A13, XREAL_1:235;
then k1 -' k2 <= (len f) -' k2 by A1, XREAL_1:235;
then (k1 -' k2) + 1 <= ((len f) -' k2) + 1 by XREAL_1:8;
then A19: ((len f) -' (k2 -' 1)) -' ((k1 -' k2) + 1) = (((len f) -' k2) + 1) - ((k1 -' k2) + 1) by A17, XREAL_1:235
.= (((len f) - k2) + 1) - ((k1 - k2) + 1) by A13, A14, XREAL_1:235
.= (((len f) + 1) - 1) - k1
.= (len f) -' k1 by A1, XREAL_1:235 ;
A20: (len f) -' k2 >= (len f) -' k1 by A13, NAT_D:41;
(len f) -' k2 <= ((len f) -' k2) + 1 by NAT_1:11;
then A21: ((len f) -' (k2 -' 1)) -' ((len f) -' k1) = (((len f) -' k2) + 1) - ((len f) -' k1) by A17, A20, XREAL_1:235, XXREAL_0:2
.= (((len f) - k2) + 1) - ((len f) - k1) by A1, A14, XREAL_1:235
.= (k1 - k2) + 1
.= (k1 -' k2) + 1 by A13, XREAL_1:235 ;
A22: ((len (f /^ (k2 -' 1))) -' ((k1 -' k2) + 1)) + ((k1 -' k2) + 1) = ((len f) -' k1) + ((k1 -' k2) + 1) by A19, RFINSEQ:42
.= ((len f) - k1) + ((k1 - k2) + 1) by A13, A15, XREAL_1:235
.= (len f) - (k2 - 1)
.= (len f) - (k2 -' 1) by A1, XREAL_1:235
.= (len f) -' (k2 -' 1) by A1, NAT_D:50, XREAL_1:235
.= len (f /^ (k2 -' 1)) by RFINSEQ:42 ;
A23: ((((len f) -' k2) + 1) -' (((len f) -' k1) + 1)) + 1 = ((((len f) -' k2) + 1) - (((len f) -' k1) + 1)) + 1 by A18, XREAL_1:235
.= ((((len f) - k2) + 1) - (((len f) - k1) + 1)) + 1 by A1, A14, XREAL_1:235
.= (k1 - k2) + 1
.= (k1 -' k2) + 1 by A13, XREAL_1:235 ;
(len f) - k2 > (len f) - k1 by A13, XREAL_1:12;
then ((len f) -' k2) + 1 > ((len f) -' k1) + 1 by A14, A15, XREAL_1:8;
then mid (Rev f),(((len f) -' k2) + 1),(((len f) -' k1) + 1) = Rev (((Rev f) /^ ((((len f) -' k1) + 1) -' 1)) | ((k1 -' k2) + 1)) by A23, Def1
.= Rev (((Rev f) /^ ((len f) -' k1)) | (((len f) -' (k2 -' 1)) -' ((len f) -' k1))) by A21, NAT_D:34
.= Rev (((Rev f) | ((len f) -' (k2 -' 1))) /^ ((len f) -' k1)) by FINSEQ_5:83
.= Rev (((Rev f) | ((len f) -' (k2 -' 1))) /^ ((len (f /^ (k2 -' 1))) -' ((k1 -' k2) + 1))) by A19, RFINSEQ:42
.= Rev ((Rev (f /^ (k2 -' 1))) /^ ((len (f /^ (k2 -' 1))) -' ((k1 -' k2) + 1))) by A16, FINSEQ_6:90
.= Rev (Rev ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1))) by A22, FINSEQ_6:91
.= Rev (mid f,k1,k2) by A13, Def1 ;
hence Rev (mid f,k1,k2) = mid (Rev f),(((len f) -' k2) + 1),(((len f) -' k1) + 1) ; :: thesis: verum

end;

end;