let r be Real; :: thesis: ( - 1 <= r & r <= 1 implies cot (arctan r) = 1 / r )
set x = arctan r;
assume A1: ( - 1 <= r & r <= 1 ) ; :: thesis: cot (arctan r) = 1 / r
A4: (sin (arctan r)) / (cos (arctan r)) = tan (arctan r) by SIN_COS4:def 1
.= r by A1, Th49 ;
cot (arctan r) = (cos (arctan r)) / (sin (arctan r)) by SIN_COS4:def 2
.= 1 / r by A4, XCMPLX_1:57 ;
hence cot (arctan r) = 1 / r ; :: thesis: verum