theorem :: FINSEQ_6:119
for f being FinSequence
for k1, k2 being Nat holds rng (mid (f,k1,k2)) c= rng f