theorem Th114: :: SINCOS10:114
for r being Real st - (sqrt 2) <= r & r <= - 1 holds
( sin . (arcsec2 r) = - ((sqrt ((r ^2) - 1)) / r) & cos . (arcsec2 r) = 1 / r )