theorem :: FDIFF_4:40

for Z being open Subset of REAL st ( for x being Real st x in Z holds
sin . x <> 0 ) holds
( sin ^ is_differentiable_on Z & ( for x being Real st x in Z holds
((sin ^) `| Z) . x = - ((cos . x) / ((sin . x) ^2)) ) )