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 A4, NAT_D:44;
then A5: len (f /^ (k21 -' 1)) = (len f) - (k21 -' 1) by RFINSEQ:def 1;
A6: k21 - 1 >= 0 by A3, XREAL_1:48;
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 A9, Def3
.= ((f /^ (k1 -' 1)) | (Seg ((k2 -' k1) + 1))) . 1 ;
k1 - 1 >= 0 by A10, XREAL_1:48;
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 A11, NAT_D:44;
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 A16, XBOOLE_0:def 4;
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 A12, FUNCT_1:47;
hence (mid (f,k1,k2)) . 1 = f . k1 by A13, A15, A16, RFINSEQ:def 1; :: 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 A3, XREAL_1:48;
A19: k11 - k21 >= 0 by A17, XREAL_1:48;
then k11 -' k21 = k11 - k21 by XREAL_0:def 2;
then A20: (k21 -' 1) + ((k11 -' k21) + 1) = (k21 - 1) + (k11 - (k21 - 1)) by A18, XREAL_0:def 2
.= k11 ;
k21 -' 1 <= len f by A4, NAT_D:44;
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 A19, XREAL_0:def 2
.= k11 - (k21 - 1)
.= k11 - (k21 -' 1) by A18, XREAL_0:def 2 ;
then A23: (k11 -' k21) + 1 <= len (f /^ (k21 -' 1)) by A2, A21, XREAL_1:9;
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 A22, FINSEQ_3:25;
a25: (k11 -' k21) + 1 in dom (f /^ (k21 -' 1)) by A23, FINSEQ_3:25, A22;
A26: (k11 -' k21) + 1 in dom (f /^ (k21 -' 1)) by A22, A23, FINSEQ_3:25;
A27: ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) . (len ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1))) = ((fa /^ (k21 -' 1)) | ((k11 -' k21) + 1)) /. ((k11 -' k21) + 1) by A22, A24, FINSEQ_4:15
.= (fa /^ (k21 -' 1)) /. ((k11 -' k21) + 1) by A25, FINSEQ_4:70
.= (f /^ (k21 -' 1)) . ((k11 -' k21) + 1) by a25, PARTFUN1:def 6
.= f . k11 by A20, A26, FINSEQ_5:27 ;
1 in dom ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) by A22, A24, FINSEQ_3:25;
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 A17, Def3; :: 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 A1, XREAL_1:48;
then A29: k11 -' 1 = k11 - 1 by XREAL_0:def 2;
k11 -' 1 <= len f by A2, NAT_D:44;
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 A31, XREAL_1:48;
then A34: k21 -' k11 = k21 - k11 by XREAL_0:def 2;
(k21 -' k11) + 1 = (k21 - k11) + 1 by A33, XREAL_0:def 2
.= k21 - (k11 - 1)
.= k21 - (k11 -' 1) by A28, XREAL_0:def 2 ;
then A35: (k21 -' k11) + 1 <= len (f /^ (k11 -' 1)) by A4, A30, XREAL_1:9;
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 A32, A35, A38, FINSEQ_1:59;
i + (k11 - 1) <= (k21 - (k11 - 1)) + (k11 - 1) by A32, A34, A36, A38, XREAL_1:6;
then A40: i + (k11 -' 1) <= len f by A4, A29, XXREAL_0:2;
A41: k11 <= k11 + i by NAT_1:11;
A42: i + (k11 -' 1) = i + (k11 - 1) by A28, XREAL_0:def 2
.= (i + k11) - 1
.= (i + k11) -' 1 by A1, A41, XREAL_1:233, XXREAL_0:2 ;
(mid (f,k11,k21)) . i = ((f /^ (k11 -' 1)) | ((k21 -' k11) + 1)) . i by A31, Def3
.= (f /^ (k11 -' 1)) . i by A39, FINSEQ_3:112
.= f . (i + (k11 -' 1)) by A37, A40, Th113 ;
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 A32, A35, FINSEQ_1:59; :: 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 A43, Def3;
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 A44, XREAL_0:def 2
.= k11 - (k21 - 1)
.= k11 - (k21 -' 1) by A6, XREAL_0:def 2 ;
then A48: (k11 -' k21) + 1 <= len (f /^ (k21 -' 1)) by A2, A5, XREAL_1:9;
hence A49: len (mid (f,k11,k21)) = (k11 -' k21) + 1 by A47, FINSEQ_1:59; :: 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 A48, FINSEQ_1:59;
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 A45, A49, A52, XREAL_1:6;
(k11 -' k21) + 1 <= ((k11 -' k21) + 1) + (i -' 1) by NAT_1:11;
then (k11 -' k21) + 1 <= ((k11 -' k21) + 1) + (i - 1) by A51, XREAL_1:233;
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 A47, A48, A52, FINSEQ_1:59;
then A55: (((k11 -' k21) + 1) -' i) + 1 <= (k11 -' k21) + 1 by A54, XREAL_1:233;
A56: i + k11 <= i + (len f) by A2, XREAL_1:6;
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 A49, A52, XREAL_1:233
.= (((k11 - (k21 - 1)) - i) + 1) + (k21 - 1) by A6, A45, XREAL_0:def 2
.= (k11 - i) + 1
.= (k11 -' i) + 1 by A7, A53, A57, XREAL_1:233, XXREAL_0:2 ;
1 + k11 <= i + k11 by A51, XREAL_1:6;
then 1 + k11 <= i + (len f) by A56, XXREAL_0:2;
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 A7, A53, A57, A58, XREAL_1:233, XXREAL_0:2;
(mid (f,k11,k21)) . i = ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) . (((len ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1))) - i) + 1) by A46, A47, A51, A52, Th114
.= ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) . (((len ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1))) -' i) + 1) by A47, A52, XREAL_1:233
.= (f /^ (k21 -' 1)) . ((((k11 -' k21) + 1) -' i) + 1) by A50, A55, FINSEQ_3:112
.= f . ((k11 -' i) + 1) by A58, A59, Th113, NAT_1:11 ;
hence (mid (f,k11,k21)) . i = f . ((k11 -' i) + 1) ; :: thesis: verum
end;