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
( (mid f,k1,k2) . 1 = f . k1 & ( k1 <= k2 implies ( len (mid f,k1,k2) = (k2 -' k1) + 1 & ( for i being Element of 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 Element of NAT st 1 <= i & i <= len (mid f,k1,k2) holds
(mid f,k1,k2) . i = f . ((k1 -' i) + 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
( (mid f,k1,k2) . 1 = f . k1 & ( k1 <= k2 implies ( len (mid f,k1,k2) = (k2 -' k1) + 1 & ( for i being Element of 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 Element of NAT st 1 <= i & i <= len (mid f,k1,k2) holds
(mid f,k1,k2) . i = f . ((k1 -' i) + 1) ) ) ) )
let k11, k21 be Element of 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 Element of 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 Element of NAT st 1 <= i & i <= len (mid f,k11,k21) holds
(mid f,k11,k21) . i = f . ((k11 -' i) + 1) ) ) ) ) )
assume A1:
( 1 <= k11 & k11 <= len f & 1 <= k21 & 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 Element of 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 Element of NAT st 1 <= i & i <= len (mid f,k11,k21) holds
(mid f,k11,k21) . i = f . ((k11 -' i) + 1) ) ) ) )
A2:
now let k1,
k2 be
Element of
NAT ;
:: thesis: ( k1 <= k2 & 1 <= k1 & k1 <= len f implies (mid f,k1,k2) . 1 = f . k1 )now assume A3:
(
k1 <= k2 & 1
<= k1 &
k1 <= len f )
;
:: thesis: (mid f,k1,k2) . 1 = f . k1then A4:
(mid f,k1,k2) . 1 =
((f /^ (k1 -' 1)) | ((k2 -' k1) + 1)) . 1
by Def1
.=
((f /^ (k1 -' 1)) | (Seg ((k2 -' k1) + 1))) . 1
by FINSEQ_1:def 15
;
k1 - 1
>= 0
by A3, XREAL_1:50;
then A5: 1
+ (k1 -' 1) =
1
+ (k1 - 1)
by XREAL_0:def 2
.=
k1
;
then
1
+ (k1 -' 1) <= ((len f) - (k1 -' 1)) + (k1 -' 1)
by A3;
then A6:
1
<= (len f) - (k1 -' 1)
by XREAL_1:8;
A7:
k1 -' 1
<= len f
by A3, NAT_D:44;
then A8:
len (f /^ (k1 -' 1)) = (len f) - (k1 -' 1)
by RFINSEQ:def 2;
0 + 1
<= (k2 -' k1) + 1
by XREAL_1:8;
then
( 1
in Seg ((k2 -' k1) + 1) & 1
in Seg (len (f /^ (k1 -' 1))) )
by A6, A8, FINSEQ_1:3;
then A9:
( 1
in dom (f /^ (k1 -' 1)) & 1
in Seg ((k2 -' k1) + 1) )
by FINSEQ_1:def 3;
then
1
in (dom (f /^ (k1 -' 1))) /\ (Seg ((k2 -' k1) + 1))
by XBOOLE_0:def 4;
then
1
in dom ((f /^ (k1 -' 1)) | (Seg ((k2 -' k1) + 1)))
by RELAT_1:90;
then
(mid f,k1,k2) . 1
= (f /^ (k1 -' 1)) . 1
by A4, FUNCT_1:70;
hence
(mid f,k1,k2) . 1
= f . k1
by A5, A7, A9, RFINSEQ:def 2;
:: 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 Element of 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 Element of 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 A10:
k11 > k21
;
:: thesis: (mid f,k11,k21) . 1 = f . k11A11:
1
<= (k11 -' k21) + 1
by NAT_1:11;
k21 -' 1
<= len f
by A1, NAT_D:44;
then A12:
len (f /^ (k21 -' 1)) = (len f) - (k21 -' 1)
by RFINSEQ:def 2;
A13:
k21 - 1
>= 0
by A1, XREAL_1:50;
A14:
k11 - k21 >= 0
by A10, XREAL_1:50;
then A15:
k11 -' k21 = k11 - k21
by XREAL_0:def 2;
(k11 -' k21) + 1 =
(k11 - k21) + 1
by A14, XREAL_0:def 2
.=
k11 - (k21 - 1)
.=
k11 - (k21 -' 1)
by A13, XREAL_0:def 2
;
then A16:
(k11 -' k21) + 1
<= len (f /^ (k21 -' 1))
by A1, A12, XREAL_1:11;
then A17:
len ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) = (k11 -' k21) + 1
by FINSEQ_1:80;
then A18:
(k11 -' k21) + 1
in dom ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1))
by A11, FINSEQ_3:27;
A19:
(k11 -' k21) + 1
in dom (f /^ (k21 -' 1))
by A11, A16, FINSEQ_3:27;
A20:
(k21 -' 1) + ((k11 -' k21) + 1) =
(k21 - 1) + (k11 - (k21 - 1))
by A13, A15, XREAL_0:def 2
.=
k11
;
A21:
((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) . (len ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1))) =
((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) /. ((k11 -' k21) + 1)
by A11, A17, FINSEQ_4:24
.=
(f /^ (k21 -' 1)) /. ((k11 -' k21) + 1)
by A18, FINSEQ_4:85
.=
f /. ((k21 -' 1) + ((k11 -' k21) + 1))
by A19, FINSEQ_5:30
.=
f . k11
by A1, A20, FINSEQ_4:24
;
1
in dom ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1))
by A11, A17, FINSEQ_3:27;
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:61
.=
f . k11
by A21
;
hence
(mid f,k11,k21) . 1
= f . k11
by A10, Def1;
:: thesis: verum end;
end;
thus
( k11 <= k21 implies ( len (mid f,k11,k21) = (k21 -' k11) + 1 & ( for i being Element of 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 Element of NAT st 1 <= i & i <= len (mid f,k11,k21) holds
(mid f,k11,k21) . i = f . ((k11 -' i) + 1) ) ) )proof
assume A22:
k11 <= k21
;
:: thesis: ( len (mid f,k11,k21) = (k21 -' k11) + 1 & ( for i being Element of NAT st 1 <= i & i <= len (mid f,k11,k21) holds
(mid f,k11,k21) . i = f . ((i + k11) -' 1) ) )
then A23:
mid f,
k11,
k21 = (f /^ (k11 -' 1)) | ((k21 -' k11) + 1)
by Def1;
k11 -' 1
<= len f
by A1, NAT_D:44;
then A24:
len (f /^ (k11 -' 1)) = (len f) - (k11 -' 1)
by RFINSEQ:def 2;
A25:
k11 - 1
>= 0
by A1, XREAL_1:50;
then A26:
k11 -' 1
= k11 - 1
by XREAL_0:def 2;
A27:
k21 - k11 >= 0
by A22, XREAL_1:50;
then A28:
k21 -' k11 = k21 - k11
by XREAL_0:def 2;
(k21 -' k11) + 1 =
(k21 - k11) + 1
by A27, XREAL_0:def 2
.=
k21 - (k11 - 1)
.=
k21 - (k11 -' 1)
by A25, XREAL_0:def 2
;
then A29:
(k21 -' k11) + 1
<= len (f /^ (k11 -' 1))
by A1, A24, XREAL_1:11;
then A30:
len ((f /^ (k11 -' 1)) | ((k21 -' k11) + 1)) = (k21 -' k11) + 1
by FINSEQ_1:80;
for
i being
Element of
NAT st 1
<= i &
i <= len (mid f,k11,k21) holds
(mid f,k11,k21) . i = f . ((i + k11) -' 1)
proof
let i be
Element of
NAT ;
:: thesis: ( 1 <= i & i <= len (mid f,k11,k21) implies (mid f,k11,k21) . i = f . ((i + k11) -' 1) )
assume A31:
( 1
<= i &
i <= len (mid f,k11,k21) )
;
:: thesis: (mid f,k11,k21) . i = f . ((i + k11) -' 1)
then A32:
i + (k11 - 1) <= (k21 - (k11 - 1)) + (k11 - 1)
by A23, A28, A30, XREAL_1:8;
A33:
(
i <= (k21 -' k11) + 1 &
(k21 -' k11) + 1
<= len (f /^ (k11 -' 1)) )
by A23, A29, A31, FINSEQ_1:80;
A34:
( 1
<= i &
i + (k11 -' 1) <= len f )
by A1, A26, A31, A32, XXREAL_0:2;
A35:
k11 <= k11 + i
by NAT_1:11;
A36:
i + (k11 -' 1) =
i + (k11 - 1)
by A25, XREAL_0:def 2
.=
(i + k11) - 1
.=
(i + k11) -' 1
by A1, A35, XREAL_1:235, XXREAL_0:2
;
(mid f,k11,k21) . i =
((f /^ (k11 -' 1)) | ((k21 -' k11) + 1)) . i
by A22, Def1
.=
(f /^ (k11 -' 1)) . i
by A33, FINSEQ_3:121
.=
f . (i + (k11 -' 1))
by A34, Th23
;
hence
(mid f,k11,k21) . i = f . ((i + k11) -' 1)
by A36;
:: thesis: verum
end;
hence
(
len (mid f,k11,k21) = (k21 -' k11) + 1 & ( for
i being
Element of
NAT st 1
<= i &
i <= len (mid f,k11,k21) holds
(mid f,k11,k21) . i = f . ((i + k11) -' 1) ) )
by A23, A29, FINSEQ_1:80;
:: thesis: verum
end;
assume A37:
k11 > k21
; :: thesis: ( len (mid f,k11,k21) = (k11 -' k21) + 1 & ( for i being Element of NAT st 1 <= i & i <= len (mid f,k11,k21) holds
(mid f,k11,k21) . i = f . ((k11 -' i) + 1) ) )
then A38:
mid f,k11,k21 = Rev ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1))
by Def1;
then A39:
len (mid f,k11,k21) = len ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1))
by FINSEQ_5:def 3;
k21 -' 1 <= len f
by A1, NAT_D:44;
then A40:
len (f /^ (k21 -' 1)) = (len f) - (k21 -' 1)
by RFINSEQ:def 2;
A41:
k21 - 1 >= 0
by A1, XREAL_1:50;
then A42:
k21 -' 1 = k21 - 1
by XREAL_0:def 2;
A43:
k11 - k21 >= 0
by A37, XREAL_1:50;
then A44:
k11 -' k21 = k11 - k21
by XREAL_0:def 2;
(k11 -' k21) + 1 =
(k11 - k21) + 1
by A43, XREAL_0:def 2
.=
k11 - (k21 - 1)
.=
k11 - (k21 -' 1)
by A41, XREAL_0:def 2
;
then A45:
(k11 -' k21) + 1 <= len (f /^ (k21 -' 1))
by A1, A40, XREAL_1:11;
then A46:
len ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) = (k11 -' k21) + 1
by FINSEQ_1:80;
thus A47:
len (mid f,k11,k21) = (k11 -' k21) + 1
by A39, A45, FINSEQ_1:80; :: thesis: for i being Element of NAT st 1 <= i & i <= len (mid f,k11,k21) holds
(mid f,k11,k21) . i = f . ((k11 -' i) + 1)
thus
for i being Element of NAT st 1 <= i & i <= len (mid f,k11,k21) holds
(mid f,k11,k21) . i = f . ((k11 -' i) + 1)
:: thesis: verumproof
let i be
Element of
NAT ;
:: thesis: ( 1 <= i & i <= len (mid f,k11,k21) implies (mid f,k11,k21) . i = f . ((k11 -' i) + 1) )
assume A48:
( 1
<= i &
i <= len (mid f,k11,k21) )
;
:: thesis: (mid f,k11,k21) . i = f . ((k11 -' i) + 1)
then A49:
i <= (k11 -' k21) + 1
by A39, A45, FINSEQ_1:80;
A50:
i + (k21 - 1) <= (k11 - (k21 - 1)) + (k21 - 1)
by A44, A47, A48, XREAL_1:8;
A51:
i <= i + (k21 -' 1)
by NAT_1:11;
then A52:
i <= k11
by A42, A50, XXREAL_0:2;
A53:
((((k11 -' k21) + 1) -' i) + 1) + (k21 -' 1) =
((((k11 -' k21) + 1) - i) + 1) + (k21 -' 1)
by A47, A48, XREAL_1:235
.=
(((k11 - (k21 - 1)) - i) + 1) + (k21 - 1)
by A41, A44, XREAL_0:def 2
.=
(k11 - i) + 1
.=
(k11 -' i) + 1
by A42, A50, A51, XREAL_1:235, XXREAL_0:2
;
(k11 -' k21) + 1
<= ((k11 -' k21) + 1) + (i -' 1)
by NAT_1:11;
then
(k11 -' k21) + 1
<= ((k11 -' k21) + 1) + (i - 1)
by A48, XREAL_1:235;
then
((k11 -' k21) + 1) - (i - 1) <= (((k11 -' k21) + 1) + (i - 1)) - (i - 1)
by XREAL_1:11;
then
(((k11 -' k21) + 1) - i) + 1
<= (k11 -' k21) + 1
;
then A54:
(((k11 -' k21) + 1) -' i) + 1
<= (k11 -' k21) + 1
by A49, XREAL_1:235;
A55:
1
+ k11 <= i + k11
by A48, XREAL_1:8;
i + k11 <= i + (len f)
by A1, XREAL_1:8;
then
1
+ k11 <= i + (len f)
by A55, XXREAL_0:2;
then
(1 + k11) - i <= (i + (len f)) - i
by XREAL_1:11;
then
(k11 - i) + 1
<= len f
;
then A56:
( 1
<= (((k11 -' k21) + 1) -' i) + 1 &
((((k11 -' k21) + 1) -' i) + 1) + (k21 -' 1) <= len f )
by A52, A53, NAT_1:11, XREAL_1:235;
(mid f,k11,k21) . i =
((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) . (((len ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1))) - i) + 1)
by A38, A39, A48, Th24
.=
((f /^ (k21 -' 1)) | ((k11 -' k21) + 1)) . (((len ((f /^ (k21 -' 1)) | ((k11 -' k21) + 1))) -' i) + 1)
by A39, A48, XREAL_1:235
.=
(f /^ (k21 -' 1)) . ((((k11 -' k21) + 1) -' i) + 1)
by A46, A54, FINSEQ_3:121
.=
f . ((k11 -' i) + 1)
by A53, A56, Th23
;
hence
(mid f,k11,k21) . i = f . ((k11 -' i) + 1)
;
:: thesis: verum
end;