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

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

proof

assume ].(- (PI / 2)),(- (PI / 4)).[ /\ (cos " {0 }) <> {} ; :: thesis: contradiction
then consider rr being set 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 13;
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:27;
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:27, 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 8; :: 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 8
.= 1 / (- ((sqrt ((r ^2 ) - 1)) / r)) by A5, 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