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:91;
sec . (arcsec2 r) = (sec | [.((3 / 4) * PI ),PI .]) . (arcsec2 . r) by A1, Th86, FUNCT_1:72
.= (sec | [.((3 / 4) * PI ),PI .]) . ((arcsec2 | [.(- (sqrt 2)),(- 1).]) . r) by A1, FUNCT_1:72
.= ((sec | [.((3 / 4) * PI ),PI .]) * (arcsec2 | [.(- (sqrt 2)),(- 1).])) . r by A2, FUNCT_1:23
.= (id [.(- (sqrt 2)),(- 1).]) . r by Th42, Th50, FUNCT_1:61
.= r by A1, FUNCT_1:35 ;
hence sec . (arcsec2 r) = r ; :: thesis: verum