let p be XFinSequence; for k1, k2 being Nat st 1 <= k1 & k2 <= len p holds
mid (p,k1,k2) = (p /^ (k1 -' 1)) | ((k2 + 1) -' k1)
let k1, k2 be Nat; ( 1 <= k1 & k2 <= len p implies mid (p,k1,k2) = (p /^ (k1 -' 1)) | ((k2 + 1) -' k1) )
assume that
A1:
1 <= k1
and
A2:
k2 <= len p
; mid (p,k1,k2) = (p /^ (k1 -' 1)) | ((k2 + 1) -' k1)
set k11 = k1;
set k21 = k2;
A3:
len (p | k2) = k2
by A2, AFINSQ_1:54;
k1 < k1 + 1
by NAT_1:13;
then
k1 - 1 < (k1 + 1) - 1
by XREAL_1:9;
then A4:
k1 -' 1 < k1
by A1, XREAL_1:233;
per cases
( k1 <= k2 or k1 > k2 )
;
suppose A5:
k1 <= k2
;
mid (p,k1,k2) = (p /^ (k1 -' 1)) | ((k2 + 1) -' k1)A6:
k2 < k2 + 1
by XREAL_1:29;
then A7:
(k2 + 1) -' k1 =
(k2 + 1) - k1
by A5, XREAL_1:233, XXREAL_0:2
.=
k2 - (k1 - 1)
;
A8:
k1 -' 1
= k1 - 1
by A1, XREAL_1:233;
k1 - 1
< k1
by XREAL_1:44;
then
k1 - 1
< k2
by A5, XXREAL_0:2;
then A9:
len (mid (p,k1,k2)) = k2 - (k1 - 1)
by A3, A8, Th7;
then A10:
len (mid (p,k1,k2)) = (k2 + 1) - k1
;
k1 -' 1
< k2
by A4, A5, XXREAL_0:2;
then
k1 -' 1
< len p
by A2, XXREAL_0:2;
then
len (p /^ (k1 -' 1)) = (len p) - (k1 -' 1)
by Th7;
then A11:
(k2 + 1) -' k1 <= len (p /^ (k1 -' 1))
by A2, A8, A7, XREAL_1:9;
A12:
for
i being
Nat st
i < len (mid (p,k1,k2)) holds
(mid (p,k1,k2)) . i = ((p /^ (k1 -' 1)) | ((k2 + 1) -' k1)) . i
proof
let i be
Nat;
( i < len (mid (p,k1,k2)) implies (mid (p,k1,k2)) . i = ((p /^ (k1 -' 1)) | ((k2 + 1) -' k1)) . i )
assume A13:
i < len (mid (p,k1,k2))
;
(mid (p,k1,k2)) . i = ((p /^ (k1 -' 1)) | ((k2 + 1) -' k1)) . i
then A14:
i + (k1 -' 1) in Segm k2
by NAT_1:44, A8, A9, XREAL_1:20;
i + (k1 -' 1) < (k2 - (k1 - 1)) + (k1 -' 1)
by A9, A13, XREAL_1:6;
then A15:
i + (k1 -' 1) < len p
by A2, A8, XXREAL_0:2;
i + (k1 - 1) < k2
by A9, A13, XREAL_1:20;
then A16:
((p | k2) /^ (k1 -' 1)) . i = (p | k2) . (i + (k1 -' 1))
by A3, A8, Th8;
i in (k2 + 1) -' k1
by A7, A9, A13, AFINSQ_1:86;
then ((p /^ (k1 -' 1)) | ((k2 + 1) -' k1)) . i =
(p /^ (k1 -' 1)) . i
by A11, AFINSQ_1:53
.=
p . (i + (k1 -' 1))
by A15, Th8
;
hence
(mid (p,k1,k2)) . i = ((p /^ (k1 -' 1)) | ((k2 + 1) -' k1)) . i
by A2, A16, A14, AFINSQ_1:53;
verum
end;
len ((p /^ (k1 -' 1)) | ((k2 + 1) -' k1)) = (k2 + 1) -' k1
by A11, AFINSQ_1:54;
then
len (mid (p,k1,k2)) = len ((p /^ (k1 -' 1)) | ((k2 + 1) -' k1))
by A5, A6, A10, XREAL_1:233, XXREAL_0:2;
hence
mid (
p,
k1,
k2)
= (p /^ (k1 -' 1)) | ((k2 + 1) -' k1)
by A12, AFINSQ_1:9;
verum end;