let D be non empty set ; :: thesis: for f being FinSequence of D
for k1, k2 being 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 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 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 that
A1: 1 <= k1 and
A2: k1 <= len f and
A3: 1 <= k2 and
A4: 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 A5: k1 <= k2 ; :: thesis: Rev (mid (f,k1,k2)) = mid ((Rev f),(((len f) -' k2) + 1),(((len f) -' k1) + 1))

A6: (len f) -' (k1 -' 1) = (len f) - (k1 -' 1) by A2, NAT_D:50, XREAL_1:233
.= (len f) - (k1 - 1) by A1, XREAL_1:233
.= ((len f) - k1) + 1
.= ((len f) -' k1) + 1 by A2, XREAL_1:233 ;
A7: (len f) -' k1 = (len f) - k1 by A2, XREAL_1:233;
A8: (len f) -' k2 = (len f) - k2 by A4, XREAL_1:233;
k2 - k1 <= (len f) - k1 by A4, XREAL_1:9;
then k2 -' k1 <= (len f) - k1 by A5, XREAL_1:233;
then k2 -' k1 <= (len f) -' k1 by A2, XREAL_1:233;
then (k2 -' k1) + 1 <= ((len f) -' k1) + 1 by XREAL_1:6;
then A9: ((len f) -' (k1 -' 1)) -' ((k2 -' k1) + 1) = (((len f) -' k1) + 1) - ((k2 -' k1) + 1) by A6, XREAL_1:233
.= (((len f) - k1) + 1) - ((k2 - k1) + 1) by A5, A7, XREAL_1:233
.= (((len f) + 1) - 1) - k2
.= (len f) -' k2 by A4, XREAL_1:233 ;
then A10: ((len (f /^ (k1 -' 1))) -' ((k2 -' k1) + 1)) + ((k2 -' k1) + 1) = ((len f) -' k2) + ((k2 -' k1) + 1) by RFINSEQ:29
.= ((len f) - k2) + ((k2 - k1) + 1) by A5, A8, XREAL_1:233
.= (len f) - (k1 - 1)
.= (len f) - (k1 -' 1) by A1, XREAL_1:233
.= (len f) -' (k1 -' 1) by A2, NAT_D:50, XREAL_1:233
.= len (f /^ (k1 -' 1)) by RFINSEQ:29 ;
A11: (len f) -' k1 <= ((len f) -' k1) + 1 by NAT_1:11;
(len f) -' k1 >= (len f) -' k2 by A5, NAT_D:41;
then A12: ((len f) -' (k1 -' 1)) -' ((len f) -' k2) = (((len f) -' k1) + 1) - ((len f) -' k2) by A6, A11, XREAL_1:233, XXREAL_0:2
.= (((len f) - k1) + 1) - ((len f) - k2) by A4, A7, XREAL_1:233
.= (k2 - k1) + 1
.= (k2 -' k1) + 1 by A5, XREAL_1:233 ;
A13: ((len f) -' (k1 -' 1)) + (k1 -' 1) = ((len f) - (k1 -' 1)) + (k1 -' 1) by A2, NAT_D:50, XREAL_1:233
.= len f ;
(len f) -' k1 >= (len f) -' k2 by A5, NAT_D:41;
then ((len f) -' k1) + 1 >= ((len f) -' k2) + 1 by XREAL_1:6;
then A14: ((((len f) -' k1) + 1) -' (((len f) -' k2) + 1)) + 1 = ((((len f) -' k1) + 1) - (((len f) -' k2) + 1)) + 1 by XREAL_1:233
.= ((((len f) - k1) + 1) - (((len f) - k2) + 1)) + 1 by A4, A7, XREAL_1:233
.= (k2 - k1) + 1
.= (k2 -' k1) + 1 by A5, XREAL_1:233 ;
(len f) -' k1 >= (len f) -' k2 by A5, NAT_D:41;
then ((len f) -' k1) + 1 >= ((len f) -' k2) + 1 by XREAL_1:6;
then mid ((Rev f),(((len f) -' k2) + 1),(((len f) -' k1) + 1)) = ((Rev f) /^ ((((len f) -' k2) + 1) -' 1)) | ((k2 -' k1) + 1) by A14, Def3
.= ((Rev f) /^ ((len f) -' k2)) | (((len f) -' (k1 -' 1)) -' ((len f) -' k2)) by A12, NAT_D:34
.= ((Rev f) | ((len f) -' (k1 -' 1))) /^ ((len f) -' k2) by FINSEQ_5:80
.= ((Rev f) | ((len f) -' (k1 -' 1))) /^ ((len (f /^ (k1 -' 1))) -' ((k2 -' k1) + 1)) by A9, RFINSEQ:29
.= (Rev (f /^ (k1 -' 1))) /^ ((len (f /^ (k1 -' 1))) -' ((k2 -' k1) + 1)) by A13, Th84
.= Rev ((f /^ (k1 -' 1)) | ((k2 -' k1) + 1)) by A10, Th85
.= Rev (mid (f,k1,k2)) by A5, Def3 ;
hence Rev (mid (f,k1,k2)) = mid ((Rev f),(((len f) -' k2) + 1),(((len f) -' k1) + 1)) ; :: thesis: verum

end;

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

A16: (len f) -' (k2 -' 1) = (len f) - (k2 -' 1) by A4, NAT_D:50, XREAL_1:233
.= (len f) - (k2 - 1) by A3, XREAL_1:233
.= ((len f) - k2) + 1
.= ((len f) -' k2) + 1 by A4, XREAL_1:233 ;
A17: (len f) -' k2 = (len f) - k2 by A4, XREAL_1:233;
(len f) -' k2 >= (len f) -' k1 by A15, NAT_D:41;
then ((len f) -' k2) + 1 >= ((len f) -' k1) + 1 by XREAL_1:6;
then A18: ((((len f) -' k2) + 1) -' (((len f) -' k1) + 1)) + 1 = ((((len f) -' k2) + 1) - (((len f) -' k1) + 1)) + 1 by XREAL_1:233
.= ((((len f) - k2) + 1) - (((len f) - k1) + 1)) + 1 by A2, A17, XREAL_1:233
.= (k1 - k2) + 1
.= (k1 -' k2) + 1 by A15, XREAL_1:233 ;
A19: (len f) -' k1 = (len f) - k1 by A2, XREAL_1:233;
A20: (len f) -' k2 <= ((len f) -' k2) + 1 by NAT_1:11;
(len f) -' k2 >= (len f) -' k1 by A15, NAT_D:41;
then A21: ((len f) -' (k2 -' 1)) -' ((len f) -' k1) = (((len f) -' k2) + 1) - ((len f) -' k1) by A16, A20, XREAL_1:233, XXREAL_0:2
.= (((len f) - k2) + 1) - ((len f) - k1) by A2, A17, XREAL_1:233
.= (k1 - k2) + 1
.= (k1 -' k2) + 1 by A15, XREAL_1:233 ;
A22: ((len f) -' (k2 -' 1)) + (k2 -' 1) = ((len f) - (k2 -' 1)) + (k2 -' 1) by A4, NAT_D:50, XREAL_1:233
.= len f ;
k1 - k2 <= (len f) - k2 by A2, XREAL_1:9;
then k1 -' k2 <= (len f) - k2 by A15, XREAL_1:233;
then k1 -' k2 <= (len f) -' k2 by A4, XREAL_1:233;
then (k1 -' k2) + 1 <= ((len f) -' k2) + 1 by XREAL_1:6;
then A23: ((len f) -' (k2 -' 1)) -' ((k1 -' k2) + 1) = (((len f) -' k2) + 1) - ((k1 -' k2) + 1) by A16, XREAL_1:233
.= (((len f) - k2) + 1) - ((k1 - k2) + 1) by A15, A17, XREAL_1:233
.= (((len f) + 1) - 1) - k1
.= (len f) -' k1 by A2, XREAL_1:233 ;
then A24: ((len (f /^ (k2 -' 1))) -' ((k1 -' k2) + 1)) + ((k1 -' k2) + 1) = ((len f) -' k1) + ((k1 -' k2) + 1) by RFINSEQ:29
.= ((len f) - k1) + ((k1 - k2) + 1) by A15, A19, XREAL_1:233
.= (len f) - (k2 - 1)
.= (len f) - (k2 -' 1) by A3, XREAL_1:233
.= (len f) -' (k2 -' 1) by A4, NAT_D:50, XREAL_1:233
.= len (f /^ (k2 -' 1)) by RFINSEQ:29 ;
(len f) - k2 > (len f) - k1 by A15, XREAL_1:10;
then ((len f) -' k2) + 1 > ((len f) -' k1) + 1 by A17, A19, XREAL_1:6;
then mid ((Rev f),(((len f) -' k2) + 1),(((len f) -' k1) + 1)) = Rev (((Rev f) /^ ((((len f) -' k1) + 1) -' 1)) | ((k1 -' k2) + 1)) by A18, Def3
.= 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:80
.= Rev (((Rev f) | ((len f) -' (k2 -' 1))) /^ ((len (f /^ (k2 -' 1))) -' ((k1 -' k2) + 1))) by A23, RFINSEQ:29
.= Rev ((Rev (f /^ (k2 -' 1))) /^ ((len (f /^ (k2 -' 1))) -' ((k1 -' k2) + 1))) by A22, Th84
.= Rev (Rev ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1))) by A24, Th85
.= Rev (mid (f,k1,k2)) by A15, Def3 ;
hence Rev (mid (f,k1,k2)) = mid ((Rev f),(((len f) -' k2) + 1),(((len f) -' k1) + 1)) ; :: thesis: verum

end;

end;