theorem Th115: :: SINCOS10:115

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