theorem :: FINSEQ_6:124

for f being FinSequence
for k1, k2 being Nat holds len (mid (f,k1,k2)) <= len f