theorem LM41: :: PDIFFEQ1:15

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 2, [#] REAL & ( for x being Real holds
( (f `| ([#] REAL)) . x = - (e * ((A * (sin . (e * x))) - (B * (cos . (e * x))))) & ((f `| ([#] REAL)) `| ([#] REAL)) . x = - ((e ^2) * ((A * (cos . (e * x))) + (B * (sin . (e * x))))) & (((diff (f,([#] REAL))) . 2) /. x) + ((e ^2) * (f /. x)) = 0 ) ) )