theorem Th69: :: SINCOS10:69

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