let f be FinSequence; :: thesis: 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; :: 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 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 ) ; :: 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) )
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; :: 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 A7, 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 A4, A11, XREAL_1:233; :: thesis: verum