theorem
for
C,
d,
c being
Real for
n being
Nat for
u being
Function of
(REAL 2),
REAL st ( for
x,
t being
Real holds
u /. <*x,t*> = (sin . ((n * PI) * x)) * ((C * (cos . (((n * PI) * c) * t))) + (d * (sin . (((n * PI) * c) * t)))) ) holds
(
u is_partial_differentiable_on [#] (REAL 2),
<*1*> & ( for
x,
t being
Real holds
(u `partial| (([#] (REAL 2)),<*1*>)) /. <*x,t*> = ((n * PI) * (cos . ((n * PI) * x))) * ((C * (cos . (((n * PI) * c) * t))) + (d * (sin . (((n * PI) * c) * t)))) ) &
u is_partial_differentiable_on [#] (REAL 2),
<*2*> & ( for
x,
t being
Real holds
(u `partial| (([#] (REAL 2)),<*2*>)) /. <*x,t*> = (sin . ((n * PI) * x)) * ((- ((C * ((n * PI) * c)) * (sin . (((n * PI) * c) * t)))) + ((d * ((n * PI) * c)) * (cos . (((n * PI) * 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*> = - ((((n * PI) ^2) * (sin . ((n * PI) * x))) * ((C * (cos . (((n * PI) * c) * t))) + (d * (sin . (((n * PI) * 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*> = - (((((n * PI) * c) ^2) * (sin . ((n * PI) * x))) * ((C * (cos . (((n * PI) * c) * t))) + (d * (sin . (((n * PI) * c) * t))))) ) ) ) & ( for
t being
Real holds
(
u /. <*0,t*> = 0 &
u /. <*1,t*> = 0 ) ) & ( for
x,
t being
Real holds
(u `partial| (([#] (REAL 2)),(<*2*> ^ <*2*>))) /. <*x,t*> = (c ^2) * ((u `partial| (([#] (REAL 2)),(<*1*> ^ <*1*>))) /. <*x,t*>) ) )