theorem :: FINSEQ_6:117

for f being FinSequence
for k being Nat st k <= len f holds
mid (f,k,(len f)) = f /^ (k -' 1)