A2: sec . 0 = 1 / 1 by Lm9, Th1, RFUNCT_1:def 8, SIN_COS:33
.= 1 ;
A4: sec . (PI / 4) = 1 / (1 / (sqrt 2)) by Lm9, Th1, Th29, RFUNCT_1:def 8
.= sqrt 2 ;
A6: sec . ((3 / 4) * PI ) = 1 / (- (1 / (sqrt 2))) by Lm10, Th2, Th30, RFUNCT_1:def 8
.= - (1 / (1 / (sqrt 2))) by XCMPLX_1:189
.= - (sqrt 2) ;
sec . PI = 1 / (- 1) by Lm10, Th2, RFUNCT_1:def 8, SIN_COS:81
.= - 1 ;
hence ( sec . 0 = 1 & sec . (PI / 4) = sqrt 2 & sec . ((3 / 4) * PI ) = - (sqrt 2) & sec . PI = - 1 ) by A2, A4, A6; :: thesis: verum