let r be Real; :: thesis: ( - (sqrt 2) <= r & r <= - 1 implies sec . (arcsec2 r) = r )
assume ( - (sqrt 2) <= r & r <= - 1 ) ; :: thesis: sec . (arcsec2 r) = r
then A1: r in [.(- (sqrt 2)),(- 1).] ;
then A2: r in dom (arcsec2 | [.(- (sqrt 2)),(- 1).]) by Th46, RELAT_1:62;
sec . (arcsec2 r) = (sec | [.((3 / 4) * PI),PI.]) . (arcsec2 . r) by A1, Th86, FUNCT_1:49
.= (sec | [.((3 / 4) * PI),PI.]) . ((arcsec2 | [.(- (sqrt 2)),(- 1).]) . r) by A1, FUNCT_1:49
.= ((sec | [.((3 / 4) * PI),PI.]) * (arcsec2 | [.(- (sqrt 2)),(- 1).])) . r by A2, FUNCT_1:13
.= (id [.(- (sqrt 2)),(- 1).]) . r by Th42, Th50, FUNCT_1:39
.= r by A1, FUNCT_1:18 ;
hence sec . (arcsec2 r) = r ; :: thesis: verum