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