theorem Th59: :: HFDIFF_1:59

for Z being open Subset of REAL st Z c= dom cot holds
( cot is_differentiable_on Z & cot `| Z = ((- 1) (#) ((sin ^) ^2)) | Z )