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:72;
(((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:47;
then (arctan | [.(- 1),1.]) | [.(- 1),1.] is continuous by A1, Th21, Th25, RELAT_1:115;
hence arctan | [.(- 1),1.] is continuous by FCONT_1:15; :: thesis: verum