let r be Real; :: thesis: ( 0 <= r & r < PI / 2 implies arcsec1 (sec . r) = r )
assume ( 0 <= r & r < PI / 2 ) ; :: thesis: arcsec1 (sec . r) = r
then A1: r in [.0 ,(PI / 2).[ ;
A2: dom (sec | [.0 ,(PI / 2).[) = [.0 ,(PI / 2).[ by Th1, RELAT_1:91;
arcsec1 (sec . r) = arcsec1 . ((sec | [.0 ,(PI / 2).[) . r) by A1, FUNCT_1:72
.= (id [.0 ,(PI / 2).[) . r by A1, A2, Th65, FUNCT_1:23
.= r by A1, FUNCT_1:35 ;
hence arcsec1 (sec . r) = r ; :: thesis: verum