let D be non empty set ; :: thesis: for f being FinSequence of D
for k1, k2, i being Element of 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 f be FinSequence of D; :: thesis: for k1, k2, i being Element of 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 Element of NAT ; :: thesis: ( 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 A1: ( 1 <= k1 & k1 <= k2 & k2 <= len f & 1 <= i & ( i <= (k2 -' k1) + 1 or i <= (k2 - k1) + 1 or i <= (k2 + 1) - k1 ) ) ; :: thesis: ( (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) )
then A2: 1 <= k2 by XXREAL_0:2;
A3: k1 <= len f by A1, XXREAL_0:2;
A4: i - 1 >= 1 - 1 by A1, XREAL_1:11;
i + k1 >= 1 + k1 by A1, XREAL_1:8;
then A5: (i + k1) - 1 >= (1 + k1) - 1 by XREAL_1:11;
A6: len (mid f,k1,k2) = (k2 -' k1) + 1 by A1, A2, A3, Th27;
A7: ( i <= (k2 - k1) + 1 implies i <= (k2 -' k1) + 1 ) by A1, XREAL_1:235;
(i -' 1) + k1 = (i - 1) + k1 by A4, XREAL_0:def 2
.= (i + k1) -' 1 by A5, XREAL_0:def 2 ;
hence A8: ( (mid f,k1,k2) . i = f . ((i + k1) -' 1) & (mid f,k1,k2) . i = f . ((i -' 1) + k1) ) by A1, A2, A3, A6, A7, Th27; :: thesis: ( (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 A5, XREAL_0:def 2; :: thesis: (mid f,k1,k2) . i = f . ((i - 1) + k1)
thus (mid f,k1,k2) . i = f . ((i - 1) + k1) by A1, A8, XREAL_1:235; :: thesis: verum