theorem Th30Y: :: PDIFFEQ1:22

for u, v being PartFunc of (REAL 2),REAL
for Z being Subset of (REAL 2)
for c being Real st Z is open & Z c= dom u & Z c= dom v & u is_partial_differentiable_on Z,<*1*> ^ <*1*> & u is_partial_differentiable_on Z,<*2*> ^ <*2*> & ( for x, t being Real st <*x,t*> in Z holds
(u `partial| (Z,(<*2*> ^ <*2*>))) /. <*x,t*> = (c ^2) * ((u `partial| (Z,(<*1*> ^ <*1*>))) /. <*x,t*>) ) & v is_partial_differentiable_on Z,<*1*> ^ <*1*> & v is_partial_differentiable_on Z,<*2*> ^ <*2*> & ( for x, t being Real st <*x,t*> in Z holds
(v `partial| (Z,(<*2*> ^ <*2*>))) /. <*x,t*> = (c ^2) * ((v `partial| (Z,(<*1*> ^ <*1*>))) /. <*x,t*>) ) holds
( Z c= dom (u + v) & u + v is_partial_differentiable_on Z,<*1*> ^ <*1*> & u + v is_partial_differentiable_on Z,<*2*> ^ <*2*> & ( for x, t being Real st <*x,t*> in Z holds
((u + v) `partial| (Z,(<*2*> ^ <*2*>))) /. <*x,t*> = (c ^2) * (((u + v) `partial| (Z,(<*1*> ^ <*1*>))) /. <*x,t*>) ) )