theorem :: FINSEQ_6:123

for f being FinSequence
for k, i being Nat st 1 <= i & i <= k & k <= len f holds
(mid (f,1,k)) . i = f . i