theorem Th10:
for
A,
B,
C,
d,
e,
c being
Real for
u being
Function of
(REAL 2),
REAL st ( for
x,
t being
Real holds
u /. <*x,t*> = ((A * (cos . (e * x))) + (B * (sin . (e * x)))) * ((C * (cos . ((e * c) * t))) + (d * (sin . ((e * c) * t)))) ) holds
(
u is_partial_differentiable_on [#] (REAL 2),
<*1*> & ( for
x,
t being
Real holds
(u `partial| (([#] (REAL 2)),<*1*>)) /. <*x,t*> = ((- ((A * e) * (sin . (e * x)))) + ((B * e) * (cos . (e * x)))) * ((C * (cos . ((e * c) * t))) + (d * (sin . ((e * c) * t)))) ) &
u is_partial_differentiable_on [#] (REAL 2),
<*2*> & ( for
x,
t being
Real holds
(u `partial| (([#] (REAL 2)),<*2*>)) /. <*x,t*> = ((A * (cos . (e * x))) + (B * (sin . (e * x)))) * ((- ((C * (e * c)) * (sin . ((e * c) * t)))) + ((d * (e * c)) * (cos . ((e * c) * t)))) ) &
u is_partial_differentiable_on [#] (REAL 2),
<*1*> ^ <*1*> & ( for
x,
t being
Real holds
(
(u `partial| (([#] (REAL 2)),(<*1*> ^ <*1*>))) /. <*x,t*> = - (((e ^2) * ((A * (cos . (e * x))) + (B * (sin . (e * x))))) * ((C * (cos . ((e * c) * t))) + (d * (sin . ((e * c) * t))))) &
u is_partial_differentiable_on [#] (REAL 2),
<*2*> ^ <*2*> & ( for
x,
t being
Real holds
(u `partial| (([#] (REAL 2)),(<*2*> ^ <*2*>))) /. <*x,t*> = - ((((e * c) ^2) * ((A * (cos . (e * x))) + (B * (sin . (e * x))))) * ((C * (cos . ((e * c) * t))) + (d * (sin . ((e * c) * t))))) ) ) ) & ( for
x,
t being
Real holds
(u `partial| (([#] (REAL 2)),(<*2*> ^ <*2*>))) /. <*x,t*> = (c ^2) * ((u `partial| (([#] (REAL 2)),(<*1*> ^ <*1*>))) /. <*x,t*>) ) )