theorem Th9: :: GLIB_006:5

for p being FinSequence
for n being Nat st n in dom p & n + 1 <= len p holds
mid (p,n,(n + 1)) = <*(p . n),(p . (n + 1))*>