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