theorem :: PDIFFEQ1:20

for c being Real 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*>) ) )