let r be Real; :: thesis: ( - 1 <= r & r <= 1 implies cot (arccot r) = r )
assume ( - 1 <= r & r <= 1 ) ; :: thesis: cot (arccot r) = r
then A1: r in [.(- 1),1.] by XXREAL_1:1;
then A2: r in dom (arccot | [.(- 1),1.]) by Th22, RELAT_1:91;
A3: arccot . r in [.(PI / 4),((3 / 4) * PI ).] by A1, Th48;
A4: [.(PI / 4),((3 / 4) * PI ).] c= ].0 ,PI .[ by Lm9, Lm10, XXREAL_2:def 12;
thus cot (arccot r) = cot . (arccot . r) by A3, A4, Th14
.= (cot | [.(PI / 4),((3 / 4) * PI ).]) . (arccot . r) by A1, Th48, FUNCT_1:72
.= (cot | [.(PI / 4),((3 / 4) * PI ).]) . ((arccot | [.(- 1),1.]) . r) by A1, FUNCT_1:72
.= ((cot | [.(PI / 4),((3 / 4) * PI ).]) * (arccot | [.(- 1),1.])) . r by A2, FUNCT_1:23
.= (id [.(- 1),1.]) . r by Th20, Th24, FUNCT_1:61
.= r by A1, FUNCT_1:35 ; :: thesis: verum