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