let r be Real; ( 1 <= r & r <= sqrt 2 implies sec . (arcsec1 r) = r )
assume
( 1 <= r & r <= sqrt 2 )
; sec . (arcsec1 r) = r
then A1:
r in [.1,(sqrt 2).]
;
then A2:
r in dom (arcsec1 | [.1,(sqrt 2).])
by Th45, RELAT_1:62;
sec . (arcsec1 r) =
(sec | [.0,(PI / 4).]) . (arcsec1 . r)
by A1, Th85, FUNCT_1:49
.=
(sec | [.0,(PI / 4).]) . ((arcsec1 | [.1,(sqrt 2).]) . r)
by A1, FUNCT_1:49
.=
((sec | [.0,(PI / 4).]) * (arcsec1 | [.1,(sqrt 2).])) . r
by A2, FUNCT_1:13
.=
(id [.1,(sqrt 2).]) . r
by Th41, Th49, FUNCT_1:39
.=
r
by A1, FUNCT_1:18
;
hence
sec . (arcsec1 r) = r
; verum