theorem Th43: :: FDIFF_6:43

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