theorem :: INTEGRA1:58

for i, j being Element of NAT
for f being FinSequence st i in dom f & j in dom f & i <= j holds
len (mid (f,i,j)) = (j - i) + 1 by Lm1;