let C, d, c be Real; :: thesis: 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; :: thesis: 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; :: thesis: ( ( 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)))) ; :: thesis: ( 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))))

proof

let x, t be Real; :: thesis: (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 `partial| (([#] (REAL 2)),<*1*>)) /. <*x,t*> = ((- ((0 * (n * PI)) * (sin . ((n * PI) * x)))) + ((1 * (n * PI)) * (cos . ((n * PI) * x)))) * ((C * (cos . (((n * PI) * c) * t))) + (d * (sin . (((n * PI) * c) * t)))) by AS1, Th10;
hence (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)))) ; :: thesis: verum

end;

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))))

proof

let x, t be Real; :: thesis: (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 `partial| (([#] (REAL 2)),<*2*>)) /. <*x,t*> = ((0 * (cos . ((n * PI) * x))) + (1 * (sin . ((n * PI) * x)))) * ((- ((C * ((n * PI) * c)) * (sin . (((n * PI) * c) * t)))) + ((d * ((n * PI) * c)) * (cos . (((n * PI) * c) * t)))) by AS1, Th10;
hence (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)))) ; :: thesis: verum

end;

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)))))

proof

let x, t be Real; :: thesis: (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 `partial| (([#] (REAL 2)),(<*1*> ^ <*1*>))) /. <*x,t*> = - ((((n * PI) ^2) * ((0 * (cos . ((n * PI) * x))) + (1 * (sin . ((n * PI) * x))))) * ((C * (cos . (((n * PI) * c) * t))) + (d * (sin . (((n * PI) * c) * t))))) by AS1, Th10;
hence (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))))) ; :: thesis: verum

end;

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)))))

proof

let x, t be Real; :: thesis: (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)))))
(u `partial| (([#] (REAL 2)),(<*2*> ^ <*2*>))) /. <*x,t*> = - (((((n * PI) * c) ^2) * ((0 * (cos . ((n * PI) * x))) + (1 * (sin . ((n * PI) * x))))) * ((C * (cos . (((n * PI) * c) * t))) + (d * (sin . (((n * PI) * c) * t))))) by AS1, Th10;
hence (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))))) ; :: thesis: verum

end;

for t being Real holds
( u /. <*0,t*> = 0 & u /. <*1,t*> = 0 )

proof

let t be Real; :: thesis: ( u /. <*0,t*> = 0 & u /. <*1,t*> = 0 )
thus u /. <*0,t*> = (sin . ((n * PI) * 0)) * ((C * (cos . (((n * PI) * c) * t))) + (d * (sin . (((n * PI) * c) * t)))) by AS
.= 0 by SIN_COS:30 ; :: thesis: u /. <*1,t*> = 0
thus u /. <*1,t*> = (sin . ((n * PI) * 1)) * ((C * (cos . (((n * PI) * c) * t))) + (d * (sin . (((n * PI) * c) * t)))) by AS
.= 0 * ((C * (cos . (((n * PI) * c) * t))) + (d * (sin . (((n * PI) * c) * t)))) by LMSIN1
.= 0 ; :: thesis: verum

end;

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; :: thesis: verum