let c be Real; :: thesis: ex u being PartFunc of (REAL 2),REAL st
( u is_partial_differentiable_on [#] (REAL 2),<*1*> ^ <*1*> & u is_partial_differentiable_on [#] (REAL 2),<*2*> ^ <*2*> & ( 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 = the Real;
set B = the Real;
set C = the Real;
set D = the Real;
set e = the Real;
consider f being Function of REAL,REAL such that
A1: for x being Real holds f . x = ( the Real * (cos . ( the Real * x))) + ( the Real * (sin . ( the Real * x))) by LM42;
consider g being Function of REAL,REAL such that
A2: for t being Real holds g . t = ( the Real * (cos . (( the Real * c) * t))) + ( the Real * (sin . (( the Real * c) * t))) by LM42;
F1: ( dom f = [#] REAL & dom g = [#] REAL ) by FUNCT_2:def 1;
consider u being PartFunc of (REAL 2),REAL such that
F2: ( dom u = { <*x,t*> where x, t is Real : ( x in [#] REAL & t in [#] REAL ) } & ( for x, t being Real st x in [#] REAL & t in [#] REAL holds
u /. <*x,t*> = (f /. x) * (g /. t) ) ) by LM10, F1;
u is total by PARTFUN1:def 2, F2, LMOP3;
then reconsider u = u as Function of (REAL 2),REAL ;
take u ; :: thesis: ( u is_partial_differentiable_on [#] (REAL 2),<*1*> ^ <*1*> & u is_partial_differentiable_on [#] (REAL 2),<*2*> ^ <*2*> & ( for x, t being Real holds (u `partial| (([#] (REAL 2)),(<*2*> ^ <*2*>))) /. <*x,t*> = (c ^2) * ((u `partial| (([#] (REAL 2)),(<*1*> ^ <*1*>))) /. <*x,t*>) ) )
A3: for x, t being Real holds u /. <*x,t*> = (f /. x) * (g /. t)

proof

let x, t be Real; :: thesis: u /. <*x,t*> = (f /. x) * (g /. t)
( x in [#] REAL & t in [#] REAL ) by XREAL_0:def 1;
hence u /. <*x,t*> = (f /. x) * (g /. t) by F2; :: thesis: verum

end;

X1: f is_differentiable_on 2, [#] REAL by LM41, A1;
X2: g is_differentiable_on 2, [#] REAL by LM41, A2;
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;
hence ( u is_partial_differentiable_on [#] (REAL 2),<*1*> ^ <*1*> & u is_partial_differentiable_on [#] (REAL 2),<*2*> ^ <*2*> & ( 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, LM50, A3; :: thesis: verum