theorem :: SINCOS10:101

for r being Real holds
( ( 1 <= r & r <= sqrt 2 & arcsec1 r = 0 implies r = 1 ) & ( 1 <= r & r <= sqrt 2 & arcsec1 r = PI / 4 implies r = sqrt 2 ) ) by Th31, Th89;