theorem Th117:
for
f being
FinSequence for
k1,
k2 being
Nat st 1
<= k1 &
k1 <= len f & 1
<= k2 &
k2 <= len f holds
(
(mid (f,k1,k2)) . 1
= f . k1 & (
k1 <= k2 implies (
len (mid (f,k1,k2)) = (k2 -' k1) + 1 & ( for
i being
Nat st 1
<= i &
i <= len (mid (f,k1,k2)) holds
(mid (f,k1,k2)) . i = f . ((i + k1) -' 1) ) ) ) & (
k1 > k2 implies (
len (mid (f,k1,k2)) = (k1 -' k2) + 1 & ( for
i being
Nat st 1
<= i &
i <= len (mid (f,k1,k2)) holds
(mid (f,k1,k2)) . i = f . ((k1 -' i) + 1) ) ) ) )