let r be Real; :: thesis: ( 1 <= r & r <= sqrt 2 implies sec . (arcsec1 r) = r )
assume ( 1 <= r & r <= sqrt 2 ) ; :: thesis: sec . (arcsec1 r) = r
then A1: r in [.1,(sqrt 2).] ;
then A2: r in dom (arcsec1 | [.1,(sqrt 2).]) by Th45, RELAT_1:91;
sec . (arcsec1 r) = (sec | [.0 ,(PI / 4).]) . (arcsec1 . r) by A1, Th85, FUNCT_1:72
.= (sec | [.0 ,(PI / 4).]) . ((arcsec1 | [.1,(sqrt 2).]) . r) by A1, FUNCT_1:72
.= ((sec | [.0 ,(PI / 4).]) * (arcsec1 | [.1,(sqrt 2).])) . r by A2, FUNCT_1:23
.= (id [.1,(sqrt 2).]) . r by Th41, Th49, FUNCT_1:61
.= r by A1, FUNCT_1:35 ;
hence sec . (arcsec1 r) = r ; :: thesis: verum