A4: cos . (PI / 4) <> 0 by Lm8, COMPTRIG:27;
A5: (sin . (PI / 4)) / (cos . (PI / 4)) = 1 by A4, SIN_COS:78, XCMPLX_1:60;
tan . (- (PI / 4)) = (sin . (- (PI / 4))) / (cos . (- (PI / 4))) by Lm7, Th1, RFUNCT_1:def 4
.= (- (sin . (PI / 4))) / (cos . (- (PI / 4))) by SIN_COS:33
.= (- (sin . (PI / 4))) / (cos . (PI / 4)) by SIN_COS:33
.= - 1 by A5 ;
hence ( tan . (- (PI / 4)) = - 1 & tan (- (PI / 4)) = - 1 ) by Lm7, Th13; :: thesis: verum