let A, B, C, d, e, c be Real; :: thesis:
let u be Function of (REAL 2),REAL; :: thesis:
assume AS: 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)))) ; :: thesis:
consider f being Function of REAL,REAL such that
A1: for x being Real holds f . x = (A * (cos . (e * x))) + (B * (sin . (e * x))) by LM42;
consider g being Function of REAL,REAL such that
A2: for t being Real holds g . t = (C * (cos . ((e * c) * t))) + (d * (sin . ((e * c) * t))) by LM42;
D0: ( dom f = REAL & dom g = REAL ) by FUNCT_2:def 1;
A3: for x, t being Real holds u /. <*x,t*> = (f /. x) * (g /. t)

let x, t be Real; :: thesis:
A31: f /. x = f . x by PARTFUN1:def 6, D0, XREAL_0:def 1
.= (A * (cos . (e * x))) + (B * (sin . (e * x))) by A1 ;
g /. t = g . t by PARTFUN1:def 6, D0, XREAL_0:def 1
.= (C * (cos . ((e * c) * t))) + (d * (sin . ((e * c) * t))) by A2 ;
hence u /. <*x,t*> = (f /. x) * (g /. t) by AS, A31; :: thesis:

end;

X1: f is_differentiable_on 2, [#] REAL by LM41, A1;
X2: g is_differentiable_on 2, [#] REAL by LM41, A2;
X3: for x, t being Real holds (f /. x) * (((diff (g,([#] REAL))) . 2) /. t) = ((c ^2) * (((diff (f,([#] REAL))) . 2) /. x)) * (g /. t) by LM43, A1, A2;
Y1: 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))))

let x, t be Real; :: thesis:
Y11: (u `partial| (([#] (REAL 2)),<*1*>)) /. <*x,t*> = (diff (f,x)) * (g /. t) by X1, X2, X3, LM50, A3;
Y12: (f `| ([#] REAL)) . x = - (e * ((A * (sin . (e * x))) - (B * (cos . (e * x))))) by LM41, A1;
Y13: f is_differentiable_on [#] REAL by D0, X1, DIFF2;
Y14: x in [#] REAL by XREAL_0:def 1;
g /. t = g . t by PARTFUN1:def 6, D0, XREAL_0:def 1
.= (C * (cos . ((e * c) * t))) + (d * (sin . ((e * c) * t))) by A2 ;
hence (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)))) by Y11, Y12, Y13, Y14, FDIFF_1:def 7; :: thesis:

end;

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

let x, t be Real; :: thesis:
Y12: (g `| ([#] REAL)) . t = - ((e * c) * ((C * (sin . ((e * c) * t))) - (d * (cos . ((e * c) * t))))) by LM41, A2;
Y13: g is_differentiable_on [#] REAL by D0, X2, DIFF2;
t in [#] REAL by XREAL_0:def 1;
then Y14: diff (g,t) = (g `| ([#] REAL)) . t by Y13, FDIFF_1:def 7;
f /. x = f . x by PARTFUN1:def 6, D0, XREAL_0:def 1
.= (A * (cos . (e * x))) + (B * (sin . (e * x))) by A1 ;
hence (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)))) by X1, X2, X3, LM50, A3, Y12, Y14; :: thesis:

end;

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

let x, t be Real; :: thesis:
Y11: (u `partial| (([#] (REAL 2)),(<*1*> ^ <*1*>))) /. <*x,t*> = (((diff (f,([#] REAL))) . 2) /. x) * (g /. t) by X1, X2, X3, LM50, A3;
R1: [#] REAL = dom f by FUNCT_2:def 1;
R2: f `| ([#] REAL) is_differentiable_on [#] REAL by R1, X1, DIFF2;
x in [#] REAL by XREAL_0:def 1;
then Y13: x in dom ((f `| ([#] REAL)) `| ([#] REAL)) by R2, FDIFF_1:def 7;
Y15: ((diff (f,([#] REAL))) . 2) /. x = ((f `| ([#] REAL)) `| ([#] REAL)) /. x by D0, X1, DIFF2
.= ((f `| ([#] REAL)) `| ([#] REAL)) . x by Y13, PARTFUN1:def 6
.= - ((e ^2) * ((A * (cos . (e * x))) + (B * (sin . (e * x))))) by LM41, A1 ;
g /. t = g . t by PARTFUN1:def 6, D0, XREAL_0:def 1
.= (C * (cos . ((e * c) * t))) + (d * (sin . ((e * c) * t))) by A2 ;
hence (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))))) by Y11, Y15; :: thesis:

end;

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

let x, t be Real; :: thesis:
Y11: (u `partial| (([#] (REAL 2)),(<*2*> ^ <*2*>))) /. <*x,t*> = (f /. x) * (((diff (g,([#] REAL))) . 2) /. t) by X1, X2, X3, LM50, A3;
R1: [#] REAL = dom g by FUNCT_2:def 1;
R2: g `| ([#] REAL) is_differentiable_on [#] REAL by R1, X2, DIFF2;
t in [#] REAL by XREAL_0:def 1;
then Y13: t in dom ((g `| ([#] REAL)) `| ([#] REAL)) by R2, FDIFF_1:def 7;
Y15: ((diff (g,([#] REAL))) . 2) /. t = ((g `| ([#] REAL)) `| ([#] REAL)) /. t by D0, X2, DIFF2
.= ((g `| ([#] REAL)) `| ([#] REAL)) . t by Y13, PARTFUN1:def 6
.= - (((e * c) ^2) * ((C * (cos . ((e * c) * t))) + (d * (sin . ((e * c) * t))))) by LM41, A2 ;
f /. x = f . x by PARTFUN1:def 6, D0, XREAL_0:def 1
.= (A * (cos . (e * x))) + (B * (sin . (e * x))) by A1 ;
hence (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))))) by Y11, Y15; :: thesis:

end;

hence ( 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*>) ) ) by X1, X2, X3, LM50, A3, Y1, Y2, Y3; :: thesis: