theorem Th10: :: GLIB_006:6

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