theorem Th116: :: SINCOS10:116

for r being Real st 1 <= r & r <= sqrt 2 holds
( sin . (arccosec2 r) = 1 / r & cos . (arccosec2 r) = (sqrt ((r ^2) - 1)) / r )