let r be Real; :: thesis: ( PI / 2 < r & r <= PI implies arcsec2 (sec . r) = r )
A1: dom (sec | ].(PI / 2),PI.]) = ].(PI / 2),PI.] by Th2, RELAT_1:62;
assume ( PI / 2 < r & r <= PI ) ; :: thesis: arcsec2 (sec . r) = r
then A2: r in ].(PI / 2),PI.] ;
then arcsec2 (sec . r) = arcsec2 . ((sec | ].(PI / 2),PI.]) . r) by FUNCT_1:49
.= (id ].(PI / 2),PI.]) . r by A2, A1, Th66, FUNCT_1:13
.= r by A2, FUNCT_1:18 ;
hence arcsec2 (sec . r) = r ; :: thesis: verum