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; verum