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
.= (len f) - (k1 - 1) by
.= ((len f) - k1) + 1
.= ((len f) -' k1) + 1 by ;
A7: (len f) -' k1 = (len f) - k1 by ;
A8: (len f) -' k2 = (len f) - k2 by ;
k2 - k1 <= (len f) - k1 by ;
then k2 -' k1 <= (len f) - k1 by ;
then k2 -' k1 <= (len f) -' k1 by ;
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
.= (((len f) - k1) + 1) - ((k2 - k1) + 1) by
.= (((len f) + 1) - 1) - k2
.= (len f) -' k2 by ;
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
.= (len f) - (k1 - 1)
.= (len f) - (k1 -' 1) by
.= (len f) -' (k1 -' 1) by
.= 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 ;
then A12: ((len f) -' (k1 -' 1)) -' ((len f) -' k2) = (((len f) -' k1) + 1) - ((len f) -' k2) by
.= (((len f) - k1) + 1) - ((len f) - k2) by
.= (k2 - k1) + 1
.= (k2 -' k1) + 1 by ;
A13: ((len f) -' (k1 -' 1)) + (k1 -' 1) = ((len f) - (k1 -' 1)) + (k1 -' 1) by
.= len f ;
(len f) -' k1 >= (len f) -' k2 by ;
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
.= (k2 - k1) + 1
.= (k2 -' k1) + 1 by ;
(len f) -' k1 >= (len f) -' k2 by ;
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
.= ((Rev f) /^ ((len f) -' k2)) | (((len f) -' (k1 -' 1)) -' ((len f) -' k2)) by
.= ((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
.= (Rev (f /^ (k1 -' 1))) /^ ((len (f /^ (k1 -' 1))) -' ((k2 -' k1) + 1)) by
.= Rev ((f /^ (k1 -' 1)) | ((k2 -' k1) + 1)) by
.= Rev (mid (f,k1,k2)) by ;
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
.= (len f) - (k2 - 1) by
.= ((len f) - k2) + 1
.= ((len f) -' k2) + 1 by ;
A17: (len f) -' k2 = (len f) - k2 by ;
(len f) -' k2 >= (len f) -' k1 by ;
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
.= (k1 - k2) + 1
.= (k1 -' k2) + 1 by ;
A19: (len f) -' k1 = (len f) - k1 by ;
A20: (len f) -' k2 <= ((len f) -' k2) + 1 by NAT_1:11;
(len f) -' k2 >= (len f) -' k1 by ;
then A21: ((len f) -' (k2 -' 1)) -' ((len f) -' k1) = (((len f) -' k2) + 1) - ((len f) -' k1) by
.= (((len f) - k2) + 1) - ((len f) - k1) by
.= (k1 - k2) + 1
.= (k1 -' k2) + 1 by ;
A22: ((len f) -' (k2 -' 1)) + (k2 -' 1) = ((len f) - (k2 -' 1)) + (k2 -' 1) by
.= len f ;
k1 - k2 <= (len f) - k2 by ;
then k1 -' k2 <= (len f) - k2 by ;
then k1 -' k2 <= (len f) -' k2 by ;
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
.= (((len f) - k2) + 1) - ((k1 - k2) + 1) by
.= (((len f) + 1) - 1) - k1
.= (len f) -' k1 by ;
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
.= (len f) - (k2 - 1)
.= (len f) - (k2 -' 1) by
.= (len f) -' (k2 -' 1) by
.= len (f /^ (k2 -' 1)) by RFINSEQ:29 ;
(len f) - k2 > (len f) - k1 by ;
then ((len f) -' k2) + 1 > ((len f) -' k1) + 1 by ;
then mid ((Rev f),(((len f) -' k2) + 1),(((len f) -' k1) + 1)) = Rev (((Rev f) /^ ((((len f) -' k1) + 1) -' 1)) | ((k1 -' k2) + 1)) by
.= Rev (((Rev f) /^ ((len f) -' k1)) | (((len f) -' (k2 -' 1)) -' ((len f) -' k1))) by
.= 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
.= Rev ((Rev (f /^ (k2 -' 1))) /^ ((len (f /^ (k2 -' 1))) -' ((k1 -' k2) + 1))) by
.= Rev (Rev ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1))) by
.= Rev (mid (f,k1,k2)) by ;
hence Rev (mid (f,k1,k2)) = mid ((Rev f),(((len f) -' k2) + 1),(((len f) -' k1) + 1)) ; :: thesis: verum
end;
end;