let f be FinSequence; 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; ( 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
; ( (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 for k1, k2 being Nat st k1 <= k2 & 1 <= k1 & k1 <= len f holds
(mid (f,k1,k2)) . 1 = f . k1let k1,
k2 be
Nat;
( k1 <= k2 & 1 <= k1 & k1 <= len f implies (mid (f,k1,k2)) . 1 = f . k1 )now ( 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
;
(mid (f,k1,k2)) . 1 = f . k1A12:
(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;
verum end; hence
(
k1 <= k2 & 1
<= k1 &
k1 <= len f implies
(mid (f,k1,k2)) . 1
= f . k1 )
;
verum end;
thus
(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) ) ) ) )proof
per cases
( k11 <= k21 or k11 > k21 )
;
suppose A17:
k11 > k21
;
(mid (f,k11,k21)) . 1 = f . k11A18:
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;
verum 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) ) ) )
( 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
;
( 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;
( 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))
;
(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;
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;
verum
end;
assume A43:
k11 > k21
; ( 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; 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)
verumproof
let i be
Nat;
( 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))
;
(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)
;
verum
end;