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