theorem LM412: :: PDIFFEQ1:14

for A, B, e being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = (A * (cos . (e * x))) + (B * (sin . (e * x))) ) holds
( f is_differentiable_on [#] REAL & ( for x being Real holds (f `| ([#] REAL)) . x = - (e * ((A * (sin . (e * x))) - (B * (cos . (e * x))))) ) )