let f be FinSequence; :: thesis: for k1, k2 being Nat st 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f holds
( (mid (f,k1,k2)) . 1 = f . k1 & ( k1 <= k2 implies ( len (mid (f,k1,k2)) = (k2 -' k1) + 1 & ( for i being Nat st 1 <= i & i <= len (mid (f,k1,k2)) holds
(mid (f,k1,k2)) . i = f . ((i + k1) -' 1) ) ) ) & ( k1 > k2 implies ( len (mid (f,k1,k2)) = (k1 -' k2) + 1 & ( for i being Nat st 1 <= i & i <= len (mid (f,k1,k2)) holds
(mid (f,k1,k2)) . i = f . ((k1 -' i) + 1) ) ) ) )

let k11, k21 be Nat; :: thesis: ( 1 <= k11 & k11 <= len f & 1 <= k21 & k21 <= len f implies ( (mid (f,k11,k21)) . 1 = f . k11 & ( k11 <= k21 implies ( len (mid (f,k11,k21)) = (k21 -' k11) + 1 & ( for i being Nat st 1 <= i & i <= len (mid (f,k11,k21)) holds
(mid (f,k11,k21)) . i = f . ((i + k11) -' 1) ) ) ) & ( k11 > k21 implies ( len (mid (f,k11,k21)) = (k11 -' k21) + 1 & ( for i being Nat st 1 <= i & i <= len (mid (f,k11,k21)) holds
(mid (f,k11,k21)) . i = f . ((k11 -' i) + 1) ) ) ) ) )

assume that
A1: 1 <= k11 and
A2: k11 <= len f and
A3: 1 <= k21 and
A4: k21 <= len f ; :: thesis: ( (mid (f,k11,k21)) . 1 = f . k11 & ( k11 <= k21 implies ( len (mid (f,k11,k21)) = (k21 -' k11) + 1 & ( for i being Nat st 1 <= i & i <= len (mid (f,k11,k21)) holds
(mid (f,k11,k21)) . i = f . ((i + k11) -' 1) ) ) ) & ( k11 > k21 implies ( len (mid (f,k11,k21)) = (k11 -' k21) + 1 & ( for i being Nat st 1 <= i & i <= len (mid (f,k11,k21)) holds
(mid (f,k11,k21)) . i = f . ((k11 -' i) + 1) ) ) ) )

reconsider fa = f as FinSequence of rng f by FINSEQ_1:def 4;
k21 -' 1 <= len f by ;
then A5: len (f /^ (k21 -' 1)) = (len f) - (k21 -' 1) by RFINSEQ:def 1;
A6: k21 - 1 >= 0 by ;
then A7: k21 -' 1 = k21 - 1 by XREAL_0:def 2;
A8: now :: thesis: for k1, k2 being Nat st k1 <= k2 & 1 <= k1 & k1 <= len f holds
(mid (f,k1,k2)) . 1 = f . k1
let k1, k2 be Nat; :: thesis: ( k1 <= k2 & 1 <= k1 & k1 <= len f implies (mid (f,k1,k2)) . 1 = f . k1 )
now :: thesis: ( k1 <= k2 & 1 <= k1 & k1 <= len f implies (mid (f,k1,k2)) . 1 = f . k1 )
assume that
A9: k1 <= k2 and
A10: 1 <= k1 and
A11: k1 <= len f ; :: thesis: (mid (f,k1,k2)) . 1 = f . k1
A12: (mid (f,k1,k2)) . 1 = ((f /^ (k1 -' 1)) | ((k2 -' k1) + 1)) . 1 by
.= ((f /^ (k1 -' 1)) | (Seg ((k2 -' k1) + 1))) . 1 ;
k1 - 1 >= 0 by ;
then A13: 1 + (k1 -' 1) = 1 + (k1 - 1) by XREAL_0:def 2
.= k1 ;
then 1 + (k1 -' 1) <= ((len f) - (k1 -' 1)) + (k1 -' 1) by A11;
then A14: 1 <= (len f) - (k1 -' 1) by XREAL_1:6;
A15: k1 -' 1 <= len f by ;
then len (f /^ (k1 -' 1)) = (len f) - (k1 -' 1) by RFINSEQ:def 1;
then 1 in Seg (len (f /^ (k1 -' 1))) by A14;
then A16: 1 in dom (f /^ (k1 -' 1)) by FINSEQ_1:def 3;
0 + 1 <= (k2 -' k1) + 1 by XREAL_1:6;
then 1 in Seg ((k2 -' k1) + 1) ;
then 1 in (dom (f /^ (k1 -' 1))) /\ (Seg ((k2 -' k1) + 1)) by ;
then 1 in dom ((f /^ (k1 -' 1)) | (Seg ((k2 -' k1) + 1))) by RELAT_1:61;
then (mid (f,k1,k2)) . 1 = (f /^ (k1 -' 1)) . 1 by ;
hence (mid (f,k1,k2)) . 1 = f . k1 by ; :: thesis: verum
end;
hence ( k1 <= k2 & 1 <= k1 & k1 <= len f implies (mid (f,k1,k2)) . 1 = f . k1 ) ; :: thesis: verum
end;
thus (mid (f,k11,k21)) . 1 = f . k11 :: thesis: ( ( k11 <= k21 implies ( len (mid (f,k11,k21)) = (k21 -' k11) + 1 & ( for i being Nat st 1 <= i & i <= len (mid (f,k11,k21)) holds
(mid (f,k11,k21)) . i = f . ((i + k11) -' 1) ) ) ) & ( k11 > k21 implies ( len (mid (f,k11,k21)) = (k11 -' k21) + 1 & ( for i being Nat st 1 <= i & i <= len (mid (f,k11,k21)) holds
(mid (f,k11,k21)) . i = f . ((k11 -' i) + 1) ) ) ) )
proof
per cases ( k11 <= k21 or k11 > k21 ) ;
suppose k11 <= k21 ; :: thesis: (mid (f,k11,k21)) . 1 = f . k11
hence (mid (f,k11,k21)) . 1 = f . k11 by A1, A2, A8; :: thesis: verum
end;
suppose A17: k11 > k21 ; :: thesis: (mid (f,k11,k21)) . 1 = f . k11
A18: k21 - 1 >= 0 by ;
A19: k11 - k21 >= 0 by ;
then k11 -' k21 = k11 - k21 by XREAL_0:def 2;
then A20: (k21 -' 1) + ((k11 -' k21) + 1) = (k21 - 1) + (k11 - (k21 - 1)) by
.= k11 ;
k21 -' 1 <= len f by ;
then A21: len (f /^ (k21 -' 1)) = (len f) - (k21 -' 1) by RFINSEQ:def 1;
A22: 1 <= (k11 -' k21) + 1 by NAT_1:11;
(k11 -' k21) + 1 = (k11 - k21) + 1 by
.= k11 - (k21 - 1)
.= k11 - (k21 -' 1) by ;
then A23: (k11 -' k21) + 1 <= len (f /^ (k21 -' 1)) by ;
then A24: len ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) = (k11 -' k21) + 1 by FINSEQ_1:59;
then A25: (k11 -' k21) + 1 in dom ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) by ;
a25: (k11 -' k21) + 1 in dom (f /^ (k21 -' 1)) by ;
A26: (k11 -' k21) + 1 in dom (f /^ (k21 -' 1)) by ;
A27: ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) . (len ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1))) = ((fa /^ (k21 -' 1)) | ((k11 -' k21) + 1)) /. ((k11 -' k21) + 1) by
.= (fa /^ (k21 -' 1)) /. ((k11 -' k21) + 1) by
.= (f /^ (k21 -' 1)) . ((k11 -' k21) + 1) by
.= f . k11 by ;
1 in dom ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) by ;
then (Rev ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1))) . 1 = ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) . (((len ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1))) - 1) + 1) by FINSEQ_5:58
.= f . k11 by A27 ;
hence (mid (f,k11,k21)) . 1 = f . k11 by ; :: thesis: verum
end;
end;
end;
thus ( k11 <= k21 implies ( len (mid (f,k11,k21)) = (k21 -' k11) + 1 & ( for i being Nat st 1 <= i & i <= len (mid (f,k11,k21)) holds
(mid (f,k11,k21)) . i = f . ((i + k11) -' 1) ) ) ) :: thesis: ( k11 > k21 implies ( len (mid (f,k11,k21)) = (k11 -' k21) + 1 & ( for i being Nat st 1 <= i & i <= len (mid (f,k11,k21)) holds
(mid (f,k11,k21)) . i = f . ((k11 -' i) + 1) ) ) )
proof
A28: k11 - 1 >= 0 by ;
then A29: k11 -' 1 = k11 - 1 by XREAL_0:def 2;
k11 -' 1 <= len f by ;
then A30: len (f /^ (k11 -' 1)) = (len f) - (k11 -' 1) by RFINSEQ:def 1;
assume A31: k11 <= k21 ; :: thesis: ( len (mid (f,k11,k21)) = (k21 -' k11) + 1 & ( for i being Nat st 1 <= i & i <= len (mid (f,k11,k21)) holds
(mid (f,k11,k21)) . i = f . ((i + k11) -' 1) ) )

then A32: mid (f,k11,k21) = (f /^ (k11 -' 1)) | ((k21 -' k11) + 1) by Def3;
A33: k21 - k11 >= 0 by ;
then A34: k21 -' k11 = k21 - k11 by XREAL_0:def 2;
(k21 -' k11) + 1 = (k21 - k11) + 1 by
.= k21 - (k11 - 1)
.= k21 - (k11 -' 1) by ;
then A35: (k21 -' k11) + 1 <= len (f /^ (k11 -' 1)) by ;
then A36: len ((f /^ (k11 -' 1)) | ((k21 -' k11) + 1)) = (k21 -' k11) + 1 by FINSEQ_1:59;
for i being Nat st 1 <= i & i <= len (mid (f,k11,k21)) holds
(mid (f,k11,k21)) . i = f . ((i + k11) -' 1)
proof
let i be Nat; :: thesis: ( 1 <= i & i <= len (mid (f,k11,k21)) implies (mid (f,k11,k21)) . i = f . ((i + k11) -' 1) )
assume that
A37: 1 <= i and
A38: i <= len (mid (f,k11,k21)) ; :: thesis: (mid (f,k11,k21)) . i = f . ((i + k11) -' 1)
A39: i <= (k21 -' k11) + 1 by ;
i + (k11 - 1) <= (k21 - (k11 - 1)) + (k11 - 1) by ;
then A40: i + (k11 -' 1) <= len f by ;
A41: k11 <= k11 + i by NAT_1:11;
A42: i + (k11 -' 1) = i + (k11 - 1) by
.= (i + k11) - 1
.= (i + k11) -' 1 by ;
(mid (f,k11,k21)) . i = ((f /^ (k11 -' 1)) | ((k21 -' k11) + 1)) . i by
.= (f /^ (k11 -' 1)) . i by
.= f . (i + (k11 -' 1)) by ;
hence (mid (f,k11,k21)) . i = f . ((i + k11) -' 1) by A42; :: thesis: verum
end;
hence ( len (mid (f,k11,k21)) = (k21 -' k11) + 1 & ( for i being Nat st 1 <= i & i <= len (mid (f,k11,k21)) holds
(mid (f,k11,k21)) . i = f . ((i + k11) -' 1) ) ) by ; :: thesis: verum
end;
assume A43: k11 > k21 ; :: thesis: ( len (mid (f,k11,k21)) = (k11 -' k21) + 1 & ( for i being Nat st 1 <= i & i <= len (mid (f,k11,k21)) holds
(mid (f,k11,k21)) . i = f . ((k11 -' i) + 1) ) )

then A44: k11 - k21 >= 0 by XREAL_1:48;
then A45: k11 -' k21 = k11 - k21 by XREAL_0:def 2;
A46: mid (f,k11,k21) = Rev ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) by ;
then A47: len (mid (f,k11,k21)) = len ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) by FINSEQ_5:def 3;
(k11 -' k21) + 1 = (k11 - k21) + 1 by
.= k11 - (k21 - 1)
.= k11 - (k21 -' 1) by ;
then A48: (k11 -' k21) + 1 <= len (f /^ (k21 -' 1)) by ;
hence A49: len (mid (f,k11,k21)) = (k11 -' k21) + 1 by ; :: thesis: for i being Nat st 1 <= i & i <= len (mid (f,k11,k21)) holds
(mid (f,k11,k21)) . i = f . ((k11 -' i) + 1)

A50: len ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) = (k11 -' k21) + 1 by ;
thus for i being Nat st 1 <= i & i <= len (mid (f,k11,k21)) holds
(mid (f,k11,k21)) . i = f . ((k11 -' i) + 1) :: thesis: verum
proof
let i be Nat; :: thesis: ( 1 <= i & i <= len (mid (f,k11,k21)) implies (mid (f,k11,k21)) . i = f . ((k11 -' i) + 1) )
assume that
A51: 1 <= i and
A52: i <= len (mid (f,k11,k21)) ; :: thesis: (mid (f,k11,k21)) . i = f . ((k11 -' i) + 1)
A53: i + (k21 - 1) <= (k11 - (k21 - 1)) + (k21 - 1) by ;
(k11 -' k21) + 1 <= ((k11 -' k21) + 1) + (i -' 1) by NAT_1:11;
then (k11 -' k21) + 1 <= ((k11 -' k21) + 1) + (i - 1) by ;
then ((k11 -' k21) + 1) - (i - 1) <= (((k11 -' k21) + 1) + (i - 1)) - (i - 1) by XREAL_1:9;
then A54: (((k11 -' k21) + 1) - i) + 1 <= (k11 -' k21) + 1 ;
i <= (k11 -' k21) + 1 by ;
then A55: (((k11 -' k21) + 1) -' i) + 1 <= (k11 -' k21) + 1 by ;
A56: i + k11 <= i + (len f) by ;
A57: i <= i + (k21 -' 1) by NAT_1:11;
A58: ((((k11 -' k21) + 1) -' i) + 1) + (k21 -' 1) = ((((k11 -' k21) + 1) - i) + 1) + (k21 -' 1) by
.= (((k11 - (k21 - 1)) - i) + 1) + (k21 - 1) by
.= (k11 - i) + 1
.= (k11 -' i) + 1 by ;
1 + k11 <= i + k11 by ;
then 1 + k11 <= i + (len f) by ;
then (1 + k11) - i <= (i + (len f)) - i by XREAL_1:9;
then (k11 - i) + 1 <= len f ;
then A59: ((((k11 -' k21) + 1) -' i) + 1) + (k21 -' 1) <= len f by ;
(mid (f,k11,k21)) . i = ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) . (((len ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1))) - i) + 1) by
.= ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) . (((len ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1))) -' i) + 1) by
.= (f /^ (k21 -' 1)) . ((((k11 -' k21) + 1) -' i) + 1) by
.= f . ((k11 -' i) + 1) by ;
hence (mid (f,k11,k21)) . i = f . ((k11 -' i) + 1) ; :: thesis: verum
end;