theorem :: FINSEQ_6:116

for f being FinSequence
for k being Nat st 1 <= k holds
mid (f,1,k) = f | k