theorem :: PDIFFEQ1:23

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