let r be Real; :: thesis: ( 1 < r & r < sqrt 2 implies cosec . (arcsec1 r) = r / (sqrt ((r ^2 ) - 1)) )
set x = arcsec1 r;
assume A1: ( 1 < r & r < sqrt 2 ) ; :: thesis: cosec . (arcsec1 r) = r / (sqrt ((r ^2 ) - 1))
then ( 0 < arcsec1 r & arcsec1 r < PI / 4 ) by Th109;
then A2: arcsec1 r in ].0 ,(PI / 4).[ ;
PI / 4 < PI / 2 by XREAL_1:78;
then A3: ].0 ,(PI / 4).[ c= ].0 ,(PI / 2).[ by XXREAL_1:46;
].0 ,(PI / 2).] = ].0 ,(PI / 2).[ \/ {(PI / 2)} by XXREAL_1:132;
then ].0 ,(PI / 2).[ c= ].0 ,(PI / 2).] by XBOOLE_1:7;
then ].0 ,(PI / 4).[ c= ].0 ,(PI / 2).] by A3, XBOOLE_1:1;
then A4: ].0 ,(PI / 4).[ c= dom cosec by Th4, XBOOLE_1:1;
cosec . (arcsec1 r) = 1 / (sin . (arcsec1 r)) by A2, A4, RFUNCT_1:def 8
.= 1 / ((sqrt ((r ^2 ) - 1)) / r) by A1, Th113
.= r / (sqrt ((r ^2 ) - 1)) by XCMPLX_1:57 ;
hence cosec . (arcsec1 r) = r / (sqrt ((r ^2 ) - 1)) ; :: thesis: verum