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