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:62;
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:49
.= (id [.0,(PI / 2).[) . r by A2, A1, Th65, FUNCT_1:13
.= r by A2, FUNCT_1:18 ;
hence arcsec1 (sec . r) = r ; :: thesis: verum