set f = tan | [.(- (PI / 4)),(PI / 4).];
A1: (tan | [.(- (PI / 4)),(PI / 4).]) | [.(- (PI / 4)),(PI / 4).] = tan | [.(- (PI / 4)),(PI / 4).] by RELAT_1:101;
(((tan | [.(- (PI / 4)),(PI / 4).]) | [.(- (PI / 4)),(PI / 4).]) " ) | ((tan | [.(- (PI / 4)),(PI / 4).]) .: [.(- (PI / 4)),(PI / 4).]) is continuous by Lm11, Lm13, FCONT_1:54;
then (arctan | [.(- 1),1.]) | [.(- 1),1.] is continuous by A1, Th21, Th25, RELAT_1:148;
hence arctan | [.(- 1),1.] is continuous by FCONT_1:16; :: thesis: verum