cos . (PI / 4) <> 0
by Lm8, COMPTRIG:11;
then A1:
(sin . (PI / 4)) / (cos . (PI / 4)) = 1
by SIN_COS:73, XCMPLX_1:60;
tan . (- (PI / 4)) =
(sin . (- (PI / 4))) / (cos . (- (PI / 4)))
by Lm7, Th1, RFUNCT_1:def 1
.=
(- (sin . (PI / 4))) / (cos . (- (PI / 4)))
by SIN_COS:30
.=
(- (sin . (PI / 4))) / (cos . (PI / 4))
by SIN_COS:30
.=
- 1
by A1
;
hence
( tan . (- (PI / 4)) = - 1 & tan (- (PI / 4)) = - 1 )
by Lm7, Th13; verum