theorem Th121:
for
f being
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) )