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