let r be Real; :: thesis: ( - (sqrt 2) < r & r < - 1 implies cosec . (arcsec2 r) = - (r / (sqrt ((r ^2 ) - 1))) )
set x = arcsec2 r;
assume A1: ( - (sqrt 2) < r & r < - 1 ) ; :: thesis: cosec . (arcsec2 r) = - (r / (sqrt ((r ^2 ) - 1)))
then ( (3 / 4) * PI < arcsec2 r & arcsec2 r < PI ) by Th110;
then A2: arcsec2 r in ].((3 / 4) * PI ),PI .[ ;
AA: ].((3 / 4) * PI ),PI .[ c= dom cosec

proof

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

proof

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

end;

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

end;

cosec . (arcsec2 r) = 1 / (sin . (arcsec2 r)) by A2, AA, RFUNCT_1:def 8
.= 1 / (- ((sqrt ((r ^2 ) - 1)) / r)) by A1, Th114
.= - (1 / ((sqrt ((r ^2 ) - 1)) / r)) by XCMPLX_1:189
.= - (r / (sqrt ((r ^2 ) - 1))) by XCMPLX_1:57 ;
hence cosec . (arcsec2 r) = - (r / (sqrt ((r ^2 ) - 1))) ; :: thesis: verum