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 PI / 4 < (PI / 4) * 3 by XREAL_1:157;
then A1: (((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 Lm12, Lm14, FCONT_1:54;
(cot | [.(PI / 4),((3 / 4) * PI ).]) | [.(PI / 4),((3 / 4) * PI ).] = cot | [.(PI / 4),((3 / 4) * PI ).] by RELAT_1:101;
then (arccot | [.(- 1),1.]) | [.(- 1),1.] is continuous by A1, Th22, Th26, RELAT_1:148;
hence arccot | [.(- 1),1.] is continuous by FCONT_1:16; :: thesis: verum