theorem :: FDIFF_6:44

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