A1: sec . PI = 1 / (- 1) by Lm6, Th2, RFUNCT_1:def 2, SIN_COS:76
.= - 1 ;
A2: sec . ((3 / 4) * PI) = 1 / (- (1 / (sqrt 2))) by Lm6, Th2, Th30, RFUNCT_1:def 2
.= - (1 / (1 / (sqrt 2))) by XCMPLX_1:188
.= - (sqrt 2) ;
A3: sec . 0 = 1 / 1 by Lm5, Th1, RFUNCT_1:def 2, SIN_COS:30
.= 1 ;
sec . (PI / 4) = 1 / (1 / (sqrt 2)) by Lm5, Th1, Th29, RFUNCT_1:def 2
.= 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