let A, B, C, d, c, e be Real; :: thesis: 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)
let f, g be Function of REAL,REAL; :: thesis: ( ( 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))) ) implies for x, t being Real holds (f /. x) * (((diff (g,([#] REAL))) . 2) /. t) = ((c ^2) * (((diff (f,([#] REAL))) . 2) /. x)) * (g /. t) )
assume AS: ( ( 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))) ) ) ; :: thesis: for x, t being Real holds (f /. x) * (((diff (g,([#] REAL))) . 2) /. t) = ((c ^2) * (((diff (f,([#] REAL))) . 2) /. x)) * (g /. t)
let x, t be Real; :: thesis: (f /. x) * (((diff (g,([#] REAL))) . 2) /. t) = ((c ^2) * (((diff (f,([#] REAL))) . 2) /. x)) * (g /. t)
(((diff (f,([#] REAL))) . 2) /. x) + ((e ^2) * (f /. x)) = 0 by AS, LM41;
then Q3: ((c ^2) * (((diff (f,([#] REAL))) . 2) /. x)) * (g /. t) = ((c ^2) * (- ((e ^2) * (f /. x)))) * (g /. t)
.= - ((((c ^2) * (e ^2)) * (f /. x)) * (g /. t)) ;
(((diff (g,([#] REAL))) . 2) /. t) + (((e * c) ^2) * (g /. t)) = 0 by AS, LM41;
then (f /. x) * (((diff (g,([#] REAL))) . 2) /. t) = (f /. x) * (- (((e * c) ^2) * (g /. t)))
.= (f /. x) * (- (((e * c) * (e * c)) * (g /. t))) by SQUARE_1:def 1
.= (f /. x) * (- (((e * e) * (c * c)) * (g /. t)))
.= (f /. x) * (- (((e ^2) * (c * c)) * (g /. t))) by SQUARE_1:def 1
.= (f /. x) * (- (((e ^2) * (c ^2)) * (g /. t))) by SQUARE_1:def 1
.= - ((((c ^2) * (e ^2)) * (f /. x)) * (g /. t)) ;
hence (f /. x) * (((diff (g,([#] REAL))) . 2) /. t) = ((c ^2) * (((diff (f,([#] REAL))) . 2) /. x)) * (g /. t) by Q3; :: thesis: verum