set f = cot | [.(PI / 4),((3 / 4) * PI).];
PI / 4 < (PI / 4) * 3 by XREAL_1:155;
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:47;
(cot | [.(PI / 4),((3 / 4) * PI).]) | [.(PI / 4),((3 / 4) * PI).] = cot | [.(PI / 4),((3 / 4) * PI).] by RELAT_1:72;
then (arccot | [.(- 1),1.]) | [.(- 1),1.] is continuous by A1, Th22, Th26, RELAT_1:115;
hence arccot | [.(- 1),1.] is continuous by FCONT_1:15; :: thesis: verum