let u be Functional_Sequence of (REAL 2),REAL; :: thesis: 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*>) ) )
let Z be Subset of (REAL 2); :: thesis: 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*>) ) )
let c be Real; :: thesis: ( 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*>) ) ) ) implies 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*>) ) ) )
assume that
AS1: Z is open and
AS2: 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*>) ) ) ; :: thesis: 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*>) ) )
defpred S₁[ Nat] means ( Z c= dom ((Partial_Sums u) . $1) & (Partial_Sums u) . $1 is_partial_differentiable_on Z,<*1*> ^ <*1*> & (Partial_Sums u) . $1 is_partial_differentiable_on Z,<*2*> ^ <*2*> & ( for x, t being Real st <*x,t*> in Z holds
(((Partial_Sums u) . $1) `partial| (Z,(<*2*> ^ <*2*>))) /. <*x,t*> = (c ^2) * ((((Partial_Sums u) . $1) `partial| (Z,(<*1*> ^ <*1*>))) /. <*x,t*>) ) );
A9: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
set s = (Partial_Sums u) . i;
set v = u . (i + 1);
assume that
A11: Z c= dom ((Partial_Sums u) . i) and
A12: (Partial_Sums u) . i is_partial_differentiable_on Z,<*1*> ^ <*1*> and
A13: (Partial_Sums u) . i is_partial_differentiable_on Z,<*2*> ^ <*2*> and
A14: 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*>) ; :: thesis: S₁[i + 1]
A15: (Partial_Sums u) . (i + 1) = ((Partial_Sums u) . i) + (u . (i + 1)) by MESFUN9C:def 2;
( Z c= dom (u . (i + 1)) & dom (u . (i + 1)) = dom (u . 0) & u . (i + 1) is_partial_differentiable_on Z,<*1*> ^ <*1*> & u . (i + 1) is_partial_differentiable_on Z,<*2*> ^ <*2*> & ( for x, t being Real st <*x,t*> in Z holds
((u . (i + 1)) `partial| (Z,(<*2*> ^ <*2*>))) /. <*x,t*> = (c ^2) * (((u . (i + 1)) `partial| (Z,(<*1*> ^ <*1*>))) /. <*x,t*>) ) ) by AS2;
hence S₁[i + 1] by Th30Y, A11, A12, A13, A14, AS1, A15; :: thesis: verum

end;

(Partial_Sums u) . 0 = u . 0 by MESFUN9C:def 2;
then A10: S₁[ 0 ] by AS2;
for n being Nat holds S₁[n] from NAT_1:sch 2(A10, A9);
hence 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*>) ) ) ; :: thesis: verum