theorem Th113: :: SINCOS10:113

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