theorem Th70: :: SINCOS10:70

for r being Real st PI / 2 < r & r <= PI holds
arcsec2 (sec . r) = r