let r be Real; :: thesis: ( - (sqrt 2) < r & r < - 1 implies sec . (arccosec1 r) = - (r / (sqrt ((r ^2 ) - 1))) )
set x = arccosec1 r;
assume A1: ( - (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 A2: arccosec1 r in ].(- (PI / 2)),(- (PI / 4)).[ ;
AA: ].(- (PI / 2)),(- (PI / 4)).[ c= dom sec

proof

set f = cos ^ ;
A3: ].(- (PI / 2)),(- (PI / 4)).[ \ (cos " {0 }) c= (dom cos ) \ (cos " {0 }) by SIN_COS:27, XBOOLE_1:33;
].(- (PI / 2)),(- (PI / 4)).[ /\ (cos " {0 }) = {}

proof

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

end;

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

end;

sec . (arccosec1 r) = 1 / (cos . (arccosec1 r)) by A2, AA, RFUNCT_1:def 8
.= 1 / (- ((sqrt ((r ^2 ) - 1)) / r)) by A1, Th115
.= - (1 / ((sqrt ((r ^2 ) - 1)) / r)) by XCMPLX_1:189
.= - (r / (sqrt ((r ^2 ) - 1))) by XCMPLX_1:57 ;
hence sec . (arccosec1 r) = - (r / (sqrt ((r ^2 ) - 1))) ; :: thesis: verum