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