theorem LM42: :: PDIFFEQ1:16

for A, B, e being Real ex f being Function of REAL,REAL st
for x being Real holds f . x = (A * (cos . (e * x))) + (B * (sin . (e * x)))