let C, d, c be 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*>) ) )
let n be 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*>) ) )
let u be Function of (REAL 2),REAL; ( ( 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)))) ) implies ( 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*>) ) ) )
assume AS:
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))))
; ( 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*>) ) )
set A = 0 ;
set B = 1;
set e = n * PI;
AS1:
for x, t being Real holds u /. <*x,t*> = ((0 * (cos . ((n * PI) * x))) + (1 * (sin . ((n * PI) * x)))) * ((C * (cos . (((n * PI) * c) * t))) + (d * (sin . (((n * PI) * c) * t))))
by AS;
Y1:
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))))
Y2:
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))))
Y3:
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)))))
Y4:
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 )
hence
( 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*>) ) )
by AS1, Th10, Y1, Y2, Y3, Y4; verum