theorem Th10: :: FINSEQ_6:188

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