let r be Real; :: thesis: ( - (sqrt 2) < r & r < - 1 implies sec . (arccosec1 r) = - (r / (sqrt ((r ^2) - 1))) )
set x = arccosec1 r;
A1: ].(- (PI / 2)),(- (PI / 4)).[ c= dom sec

proof

].(- (PI / 2)),(- (PI / 4)).[ /\ (cos " {0}) = {}

proof

assume ].(- (PI / 2)),(- (PI / 4)).[ /\ (cos " {0}) <> {} ; :: thesis: contradiction
then consider rr being object such that
A2: rr in ].(- (PI / 2)),(- (PI / 4)).[ /\ (cos " {0}) by XBOOLE_0:def 1;
rr in cos " {0} by A2, XBOOLE_0:def 4;
then A3: cos . rr in {0} by FUNCT_1:def 7;
A4: ].(- (PI / 2)),(- (PI / 4)).[ c= ].(- (PI / 2)),(PI / 2).[ by XXREAL_1:46;
rr in ].(- (PI / 2)),(- (PI / 4)).[ by A2, XBOOLE_0:def 4;
then cos . rr <> 0 by A4, COMPTRIG:11;
hence contradiction by A3, TARSKI:def 1; :: thesis: verum

end;

then ( ].(- (PI / 2)),(- (PI / 4)).[ \ (cos " {0}) c= (dom cos) \ (cos " {0}) & ].(- (PI / 2)),(- (PI / 4)).[ misses cos " {0} ) by SIN_COS:24, XBOOLE_0:def 7, XBOOLE_1:33;
then ].(- (PI / 2)),(- (PI / 4)).[ c= (dom cos) \ (cos " {0}) by XBOOLE_1:83;
hence ].(- (PI / 2)),(- (PI / 4)).[ c= dom sec by RFUNCT_1:def 2; :: thesis: verum

end;

assume A5: ( - (sqrt 2) < r & r < - 1 ) ; :: thesis: sec . (arccosec1 r) = - (r / (sqrt ((r ^2) - 1)))
then ( - (PI / 2) < arccosec1 r & arccosec1 r < - (PI / 4) ) by Th111;
then arccosec1 r in ].(- (PI / 2)),(- (PI / 4)).[ ;
then sec . (arccosec1 r) = 1 / (cos . (arccosec1 r)) by A1, RFUNCT_1:def 2
.= 1 / (- ((sqrt ((r ^2) - 1)) / r)) by A5, Th115
.= - (1 / ((sqrt ((r ^2) - 1)) / r)) by XCMPLX_1:188
.= - (r / (sqrt ((r ^2) - 1))) by XCMPLX_1:57 ;
hence sec . (arccosec1 r) = - (r / (sqrt ((r ^2) - 1))) ; :: thesis: verum