theorem :: HFDIFF_1:61

for Z being open Subset of REAL st Z c= dom cot holds
(diff (cot,Z)) . 2 = 2 (#) (((cot (#) (sin ^)) (#) (sin ^)) | Z)