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