let r be Real; :: thesis: ( 1 <= r & r <= sqrt 2 implies ( sin . (arccosec2 r) = 1 / r & cos . (arccosec2 r) = (sqrt ((r ^2 ) - 1)) / r ) )
set x = arccosec2 r;
assume A1: ( 1 <= r & r <= sqrt 2 ) ; :: thesis: ( sin . (arccosec2 r) = 1 / r & cos . (arccosec2 r) = (sqrt ((r ^2 ) - 1)) / r )
then r in [.1,(sqrt 2).] ;
then A2: arccosec2 r in dom (cosec | [.(PI / 4),(PI / 2).]) by Lm16, Th88;
A3: dom (cosec | [.(PI / 4),(PI / 2).]) c= dom cosec by RELAT_1:89;
A5: r = (sin ^ ) . (arccosec2 r) by A1, Th92
.= 1 / (sin . (arccosec2 r)) by A2, A3, RFUNCT_1:def 8 ;
r > 0 by A1;
then A7: r ^2 > 0 ;
((sin . (arccosec2 r)) ^2 ) + ((cos . (arccosec2 r)) ^2 ) = 1 by SIN_COS:31;
then A8: (cos . (arccosec2 r)) ^2 = 1 - ((sin . (arccosec2 r)) ^2 )
.= 1 - ((1 / r) * (1 / r)) by A5
.= 1 - (1 / (r ^2 )) by XCMPLX_1:103
.= ((r ^2 ) / (r ^2 )) - (1 / (r ^2 )) by A7, XCMPLX_1:60
.= ((r ^2 ) - 1) / (r ^2 ) ;
r ^2 >= 1 ^2 by A1, SQUARE_1:77;
then A9: (r ^2 ) - 1 >= 0 by XREAL_1:50;
A11: PI / 4 <= PI / 2 by Lm12, XXREAL_1:2;
A12: PI / 4 in [.(- (PI / 2)),(PI / 2).] by A11;
PI / 2 in [.(- (PI / 2)),(PI / 2).] ;
then [.(PI / 4),(PI / 2).] c= [.(- (PI / 2)),(PI / 2).] by A12, XXREAL_2:def 12;
then cos . (arccosec2 r) >= 0 by A2, Lm16, COMPTRIG:28;
then cos . (arccosec2 r) = sqrt (((r ^2 ) - 1) / (r ^2 )) by A8, SQUARE_1:def 4
.= (sqrt ((r ^2 ) - 1)) / (sqrt (r ^2 )) by A7, A9, SQUARE_1:99
.= (sqrt ((r ^2 ) - 1)) / r by A1, SQUARE_1:89 ;
hence ( sin . (arccosec2 r) = 1 / r & cos . (arccosec2 r) = (sqrt ((r ^2 ) - 1)) / r ) by A5; :: thesis: verum