theorem :: FINSEQ_6:186

for D being non empty set
for f1 being FinSequence of D
for i1, i2 being Nat st 1 <= i2 & i2 <= i1 & i1 <= len f1 holds
len (mid (f1,i2,i1)) = (i1 -' i2) + 1