set h = cot | ].0 ,PI .[;
A1:
[.(PI / 4),((3 / 4) * PI ).] c= ].0 ,PI .[
by Lm9, Lm10, XXREAL_2:def 12;
then (cot | [.(PI / 4),((3 / 4) * PI ).]) " =
((cot | ].0 ,PI .[) | [.(PI / 4),((3 / 4) * PI ).]) "
by RELAT_1:103
.=
((cot | ].0 ,PI .[) " ) | ((cot | ].0 ,PI .[) .: [.(PI / 4),((3 / 4) * PI ).])
by RFUNCT_2:40
.=
((cot | ].0 ,PI .[) " ) | (rng ((cot | ].0 ,PI .[) | [.(PI / 4),((3 / 4) * PI ).]))
by RELAT_1:148
.=
((cot | ].0 ,PI .[) " ) | [.(- 1),1.]
by A1, Th22, RELAT_1:103
;
hence
arccot | [.(- 1),1.] = (cot | [.(PI / 4),((3 / 4) * PI ).]) "
; verum