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