theorem :: FDIFF_6:38

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