let r be Real; :: thesis: ( 1 < r & r < sqrt 2 implies sec . (arccosec2 r) = r / (sqrt ((r ^2 ) - 1)) )
set x = arccosec2 r;
assume A1: ( 1 < r & r < sqrt 2 ) ; :: thesis: sec . (arccosec2 r) = r / (sqrt ((r ^2 ) - 1))
then ( PI / 4 < arccosec2 r & arccosec2 r < PI / 2 ) by Th112;
then A2: arccosec2 r in ].(PI / 4),(PI / 2).[ ;
A3: ].(PI / 4),(PI / 2).[ c= ].0 ,(PI / 2).[ by XXREAL_1:46;
[.0 ,(PI / 2).[ = ].0 ,(PI / 2).[ \/ {0 } by XXREAL_1:131;
then ].0 ,(PI / 2).[ c= [.0 ,(PI / 2).[ by XBOOLE_1:7;
then ].(PI / 4),(PI / 2).[ c= [.0 ,(PI / 2).[ by A3, XBOOLE_1:1;
then A4: ].(PI / 4),(PI / 2).[ c= dom sec by Th1, XBOOLE_1:1;
sec . (arccosec2 r) = 1 / (cos . (arccosec2 r)) by A2, A4, RFUNCT_1:def 8
.= 1 / ((sqrt ((r ^2 ) - 1)) / r) by A1, Th116
.= r / (sqrt ((r ^2 ) - 1)) by XCMPLX_1:57 ;
hence sec . (arccosec2 r) = r / (sqrt ((r ^2 ) - 1)) ; :: thesis: verum