theorem :: JORDAN1B:6

for i being Nat
for D being non empty set
for f being FinSequence of D st 1 <= i & i < len f holds
(mid (f,i,((len f) -' 1))) ^ <*(f /. (len f))*> = mid (f,i,(len f))