let r be Real; :: thesis: ( - 1 <= r & r <= 1 implies cot (arccot r) = r )
A1: [.(PI / 4),((3 / 4) * PI).] c= ].0,PI.[ by Lm9, Lm10, XXREAL_2:def 12;
assume that
A2: - 1 <= r and
A3: r <= 1 ; :: thesis: cot (arccot r) = r
A4: r in [.(- 1),1.] by A2, A3, XXREAL_1:1;
then A5: r in dom (arccot | [.(- 1),1.]) by Th24, RELAT_1:62;
arccot . r in [.(PI / 4),((3 / 4) * PI).] by A4, Th50;
hence cot (arccot r) = cot . (arccot . r) by A1, Th14
.= (cot | [.(PI / 4),((3 / 4) * PI).]) . (arccot . r) by A4, Th50, FUNCT_1:49
.= (cot | [.(PI / 4),((3 / 4) * PI).]) . ((arccot | [.(- 1),1.]) . r) by A4, FUNCT_1:49
.= ((cot | [.(PI / 4),((3 / 4) * PI).]) * (arccot | [.(- 1),1.])) . r by A5, FUNCT_1:13
.= (id [.(- 1),1.]) . r by Th22, Th26, FUNCT_1:39
.= r by A4, FUNCT_1:18 ;
:: thesis: verum