let f be FinSequence; for k1, k2, i being Nat st 1 <= k1 & k1 <= k2 & k2 <= len f & 1 <= i & ( i <= (k2 -' k1) + 1 or i <= (k2 - k1) + 1 or i <= (k2 + 1) - k1 ) holds
( (mid (f,k1,k2)) . i = f . ((i + k1) -' 1) & (mid (f,k1,k2)) . i = f . ((i -' 1) + k1) & (mid (f,k1,k2)) . i = f . ((i + k1) - 1) & (mid (f,k1,k2)) . i = f . ((i - 1) + k1) )
let k1, k2, i be Nat; ( 1 <= k1 & k1 <= k2 & k2 <= len f & 1 <= i & ( i <= (k2 -' k1) + 1 or i <= (k2 - k1) + 1 or i <= (k2 + 1) - k1 ) implies ( (mid (f,k1,k2)) . i = f . ((i + k1) -' 1) & (mid (f,k1,k2)) . i = f . ((i -' 1) + k1) & (mid (f,k1,k2)) . i = f . ((i + k1) - 1) & (mid (f,k1,k2)) . i = f . ((i - 1) + k1) ) )
assume that
A1:
1 <= k1
and
A2:
k1 <= k2
and
A3:
k2 <= len f
and
A4:
1 <= i
and
A5:
( i <= (k2 -' k1) + 1 or i <= (k2 - k1) + 1 or i <= (k2 + 1) - k1 )
; ( (mid (f,k1,k2)) . i = f . ((i + k1) -' 1) & (mid (f,k1,k2)) . i = f . ((i -' 1) + k1) & (mid (f,k1,k2)) . i = f . ((i + k1) - 1) & (mid (f,k1,k2)) . i = f . ((i - 1) + k1) )
A6:
k1 <= len f
by A2, A3, XXREAL_0:2;
i + k1 >= 1 + k1
by A4, XREAL_1:6;
then A7:
(i + k1) - 1 >= (1 + k1) - 1
by XREAL_1:9;
A8:
( i <= (k2 - k1) + 1 implies i <= (k2 -' k1) + 1 )
by A2, XREAL_1:233;
i - 1 >= 1 - 1
by A4, XREAL_1:9;
then A9: (i -' 1) + k1 =
(i - 1) + k1
by XREAL_0:def 2
.=
(i + k1) -' 1
by A7, XREAL_0:def 2
;
A10:
1 <= k2
by A1, A2, XXREAL_0:2;
then
len (mid (f,k1,k2)) = (k2 -' k1) + 1
by A1, A2, A3, A6, Th117;
hence A11:
( (mid (f,k1,k2)) . i = f . ((i + k1) -' 1) & (mid (f,k1,k2)) . i = f . ((i -' 1) + k1) )
by A1, A2, A3, A4, A5, A10, A6, A8, A9, Th117; ( (mid (f,k1,k2)) . i = f . ((i + k1) - 1) & (mid (f,k1,k2)) . i = f . ((i - 1) + k1) )
hence
(mid (f,k1,k2)) . i = f . ((i + k1) - 1)
by A7, XREAL_0:def 2; (mid (f,k1,k2)) . i = f . ((i - 1) + k1)
thus
(mid (f,k1,k2)) . i = f . ((i - 1) + k1)
by A4, A11, XREAL_1:233; verum