let r be Real; :: thesis: ( 1 <= r & r <= sqrt 2 implies ( sin . (arccosec2 r) = 1 / r & cos . (arccosec2 r) = (sqrt ((r ^2) - 1)) / r ) )
PI / 4 <= PI / 2 by Lm8, XXREAL_1:2;
then A1: PI / 4 in [.(- (PI / 2)),(PI / 2).] ;
A2: dom (cosec | [.(PI / 4),(PI / 2).]) c= dom cosec by RELAT_1:60;
set x = arccosec2 r;
assume that
A3: 1 <= r and
A4: r <= sqrt 2 ; :: thesis: ( sin . (arccosec2 r) = 1 / r & cos . (arccosec2 r) = (sqrt ((r ^2) - 1)) / r )
r in [.1,(sqrt 2).] by A3, A4;
then A5: arccosec2 r in dom (cosec | [.(PI / 4),(PI / 2).]) by Lm32, Th88;
A6: r = (sin ^) . (arccosec2 r) by A3, A4, Th92
.= 1 / (sin . (arccosec2 r)) by A5, A2, RFUNCT_1:def 2 ;
PI / 2 in [.(- (PI / 2)),(PI / 2).] ;
then [.(PI / 4),(PI / 2).] c= [.(- (PI / 2)),(PI / 2).] by A1, XXREAL_2:def 12;
then A7: cos . (arccosec2 r) >= 0 by A5, Lm32, COMPTRIG:12;
r ^2 >= 1 ^2 by A3, SQUARE_1:15;
then A8: (r ^2) - 1 >= 0 by XREAL_1:48;
((sin . (arccosec2 r)) ^2) + ((cos . (arccosec2 r)) ^2) = 1 by SIN_COS:28;
then (cos . (arccosec2 r)) ^2 = 1 - ((sin . (arccosec2 r)) ^2)
.= 1 - ((1 / r) * (1 / r)) by A6
.= 1 - (1 / (r ^2)) by XCMPLX_1:102
.= ((r ^2) / (r ^2)) - (1 / (r ^2)) by A3, XCMPLX_1:60
.= ((r ^2) - 1) / (r ^2) ;
then cos . (arccosec2 r) = sqrt (((r ^2) - 1) / (r ^2)) by A7, SQUARE_1:def 2
.= (sqrt ((r ^2) - 1)) / (sqrt (r ^2)) by A3, A8, SQUARE_1:30
.= (sqrt ((r ^2) - 1)) / r by A3, SQUARE_1:22 ;
hence ( sin . (arccosec2 r) = 1 / r & cos . (arccosec2 r) = (sqrt ((r ^2) - 1)) / r ) by A6; :: thesis: verum