let r be Real; :: thesis: ( - 1 <= r & r <= 1 implies tan (arccot r) = 1 / r )
set x = arccot r;
assume that
A1: - 1 <= r and
A2: r <= 1 ; :: thesis: tan (arccot r) = 1 / r
A3: (cos (arccot r)) / (sin (arccot r)) = cot (arccot r) by SIN_COS4:def 2
.= r by A1, A2, Th52 ;
tan (arccot r) = (sin (arccot r)) / (cos (arccot r)) by SIN_COS4:def 1
.= 1 / r by A3, XCMPLX_1:57 ;
hence tan (arccot r) = 1 / r ; :: thesis: verum