A1: cosec . (PI / 2) =
1 / 1
by Lm8, Th4, RFUNCT_1:def 2, SIN_COS:76
.=
1
;
A2: cosec . (PI / 4) =
1 / (1 / (sqrt 2))
by Lm8, Th4, Th29, RFUNCT_1:def 2
.=
sqrt 2
;
A3: cosec . (- (PI / 2)) =
1 / (sin . (- (PI / 2)))
by Lm7, Th3, RFUNCT_1:def 2
.=
1 / (- 1)
by SIN_COS:30, SIN_COS:76
.=
- 1
;
cosec . (- (PI / 4)) =
1 / (- (1 / (sqrt 2)))
by Lm7, Th3, Th30, RFUNCT_1:def 2
.=
- (1 / (1 / (sqrt 2)))
by XCMPLX_1:188
.=
- (sqrt 2)
;
hence
( cosec . (- (PI / 2)) = - 1 & cosec . (- (PI / 4)) = - (sqrt 2) & cosec . (PI / 4) = sqrt 2 & cosec . (PI / 2) = 1 )
by A3, A2, A1; verum