set f = cot | [.(PI / 4),((3 / 4) * PI ).];
PI in ].0 ,4.[ by SIN_COS:def 32;
then PI > 0 by XXREAL_1:4;
then PI / 4 > 0 / 4 by XREAL_1:76;
then A1: PI / 4 < (PI / 4) * 3 by XREAL_1:157;
A3: (cot | [.(PI / 4),((3 / 4) * PI ).]) | [.(PI / 4),((3 / 4) * PI ).] = cot | [.(PI / 4),((3 / 4) * PI ).] by RELAT_1:101;
(((cot | [.(PI / 4),((3 / 4) * PI ).]) | [.(PI / 4),((3 / 4) * PI ).]) " ) | ((cot | [.(PI / 4),((3 / 4) * PI ).]) .: [.(PI / 4),((3 / 4) * PI ).]) is continuous by A1, Lm12, Lm14, FCONT_1:54;
then (arccot | [.(- 1),1.]) | [.(- 1),1.] is continuous by A3, Th20, Th24, RELAT_1:148;
hence arccot | [.(- 1),1.] is continuous by FCONT_1:16; :: thesis: verum