theorem :: FDIFF_7:51

for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom ((cos / sin) * f) & ( for x being Real st x in Z holds
( f . x = x / 2 & sin . (f . x) <> 0 ) ) holds
( (cos / sin) * f is_differentiable_on Z & ( for x being Real st x in Z holds
(((cos / sin) * f) `| Z) . x = - (1 / (1 - (cos . x))) ) )