theorem LM50: :: PDIFFEQ1:18

for c being Real
for f, g being Function of REAL,REAL
for u being Function of (REAL 2),REAL st f is_differentiable_on 2, [#] REAL & g is_differentiable_on 2, [#] REAL & ( for x, t being Real holds (f /. x) * (((diff (g,([#] REAL))) . 2) /. t) = ((c ^2) * (((diff (f,([#] REAL))) . 2) /. x)) * (g /. t) ) & ( for x, t being Real holds u /. <*x,t*> = (f /. x) * (g /. t) ) holds
( u is_partial_differentiable_on [#] (REAL 2),<*1*> & ( for x, t being Real holds (u `partial| (([#] (REAL 2)),<*1*>)) /. <*x,t*> = (diff (f,x)) * (g /. t) ) & u is_partial_differentiable_on [#] (REAL 2),<*2*> & ( for x, t being Real holds (u `partial| (([#] (REAL 2)),<*2*>)) /. <*x,t*> = (f /. x) * (diff (g,t)) ) & f is_differentiable_on 2, [#] REAL & g is_differentiable_on 2, [#] REAL & u is_partial_differentiable_on [#] (REAL 2),<*1*> ^ <*1*> & ( for x, t being Real holds (u `partial| (([#] (REAL 2)),(<*1*> ^ <*1*>))) /. <*x,t*> = (((diff (f,([#] REAL))) . 2) /. x) * (g /. t) ) & u is_partial_differentiable_on [#] (REAL 2),<*2*> ^ <*2*> & ( for x, t being Real holds (u `partial| (([#] (REAL 2)),(<*2*> ^ <*2*>))) /. <*x,t*> = (f /. x) * (((diff (g,([#] REAL))) . 2) /. 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*>) ) )