theorem LM43: :: PDIFFEQ1:17

for A, B, C, d, c, e being Real
for f, g being Function of REAL,REAL st ( for x being Real holds f . x = (A * (cos . (e * x))) + (B * (sin . (e * x))) ) & ( for t being Real holds g . t = (C * (cos . ((e * c) * t))) + (d * (sin . ((e * c) * t))) ) holds
for x, t being Real holds (f /. x) * (((diff (g,([#] REAL))) . 2) /. t) = ((c ^2) * (((diff (f,([#] REAL))) . 2) /. x)) * (g /. t)