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: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 ; :: thesis: verum