let r be Real; ( - 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
; 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
;
verum