let x be Real; :: thesis: ( x in ].0 ,PI .[ implies diff cot ,x = - (1 / ((sin . x) ^2 )) )
assume x in ].0 ,PI .[ ; :: thesis: diff cot ,x = - (1 / ((sin . x) ^2 ))
then sin . x <> 0 by COMPTRIG:23;
hence diff cot ,x = - (1 / ((sin . x) ^2 )) by FDIFF_7:47; :: thesis: verum