let r be Real; ( 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 )
; 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
; verum