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; :: thesis: verum