let Rseq be Function of [:NAT,NAT:],REAL; :: thesis: ( Partial_Sums Rseq is convergent_in_cod2 iff Partial_Sums_in_cod2 Rseq is convergent_in_cod2 )

hereby :: thesis: ( Partial_Sums_in_cod2 Rseq is convergent_in_cod2 implies Partial_Sums Rseq is convergent_in_cod2 )

assume A1: Partial_Sums Rseq is convergent_in_cod2 ; :: thesis: Partial_Sums_in_cod2 Rseq is convergent_in_cod2

now :: thesis: for m being Element of NAT holds ProjMap1 ((Partial_Sums_in_cod2 Rseq),m) is convergent

let m be Element of NAT ; :: thesis: ProjMap1 ((Partial_Sums_in_cod2 Rseq),m) is convergent
defpred S₁[ Nat] means for k being Element of NAT st k = $1 holds
ProjMap1 ((Partial_Sums_in_cod2 Rseq),k) is convergent ;

now :: thesis: for k being Element of NAT st k = 0 holds
ProjMap1 ((Partial_Sums_in_cod2 Rseq),k) is convergent

let k be Element of NAT ; :: thesis: ( k = 0 implies ProjMap1 ((Partial_Sums_in_cod2 Rseq),k) is convergent )
assume k = 0 ; :: thesis: ProjMap1 ((Partial_Sums_in_cod2 Rseq),k) is convergent
then ProjMap1 ((Partial_Sums Rseq),k) = ProjMap1 ((Partial_Sums_in_cod2 Rseq),k) by th00;
hence ProjMap1 ((Partial_Sums_in_cod2 Rseq),k) is convergent by A1; :: thesis: verum

end;

then A3: S₁[ 0 ] ;
A4: for m1 being Nat st S₁[m1] holds
S₁[m1 + 1]

proof

let m1 be Nat; :: thesis: ( S₁[m1] implies S₁[m1 + 1] )
reconsider m = m1 as Element of NAT by ORDINAL1:def 12;
assume S₁[m1] ; :: thesis: S₁[m1 + 1]

hereby :: thesis: verum

let k be Element of NAT ; :: thesis: ( k = m1 + 1 implies ProjMap1 ((Partial_Sums_in_cod2 Rseq),k) is convergent )
assume B2: k = m1 + 1 ; :: thesis: ProjMap1 ((Partial_Sums_in_cod2 Rseq),k) is convergent
then reconsider k1 = k - 1 as Element of NAT by NAT_1:11, NAT_1:21;
B4: ( ProjMap1 ((Partial_Sums Rseq),m) is convergent & ProjMap1 ((Partial_Sums Rseq),k) is convergent ) by A1;

now :: thesis: for e being Real st 0 < e holds
ex N being Nat st
for n being Nat st n >= N holds
|.(((ProjMap1 ((Partial_Sums_in_cod2 Rseq),k)) . n) - ((lim (ProjMap1 ((Partial_Sums Rseq),k))) - (lim (ProjMap1 ((Partial_Sums Rseq),m))))).| < e

let e be Real; :: thesis: ( 0 < e implies ex N being Nat st
for n being Nat st n >= N holds
|.(((ProjMap1 ((Partial_Sums_in_cod2 Rseq),k)) . n) - ((lim (ProjMap1 ((Partial_Sums Rseq),k))) - (lim (ProjMap1 ((Partial_Sums Rseq),m))))).| < e )
assume B6: 0 < e ; :: thesis: ex N being Nat st
for n being Nat st n >= N holds
|.(((ProjMap1 ((Partial_Sums_in_cod2 Rseq),k)) . n) - ((lim (ProjMap1 ((Partial_Sums Rseq),k))) - (lim (ProjMap1 ((Partial_Sums Rseq),m))))).| < e
then consider N1 being Nat such that
B7: for n being Nat st n >= N1 holds
|.(((ProjMap1 ((Partial_Sums Rseq),m)) . n) - (lim (ProjMap1 ((Partial_Sums Rseq),m)))).| < e / 2 by B4, SEQ_2:def 7;
consider N2 being Nat such that
B8: for n being Nat st n >= N2 holds
|.(((ProjMap1 ((Partial_Sums Rseq),k)) . n) - (lim (ProjMap1 ((Partial_Sums Rseq),k)))).| < e / 2 by B4, B6, SEQ_2:def 7;
reconsider N = max (N1,N2) as Nat by TARSKI:1;
take N = N; :: thesis: for n being Nat st n >= N holds
|.(((ProjMap1 ((Partial_Sums_in_cod2 Rseq),k)) . n) - ((lim (ProjMap1 ((Partial_Sums Rseq),k))) - (lim (ProjMap1 ((Partial_Sums Rseq),m))))).| < e

hereby :: thesis: verum

let n be Nat; :: thesis: ( n >= N implies |.(((ProjMap1 ((Partial_Sums_in_cod2 Rseq),k)) . n) - ((lim (ProjMap1 ((Partial_Sums Rseq),k))) - (lim (ProjMap1 ((Partial_Sums Rseq),m))))).| < e )
assume B9: n >= N ; :: thesis: |.(((ProjMap1 ((Partial_Sums_in_cod2 Rseq),k)) . n) - ((lim (ProjMap1 ((Partial_Sums Rseq),k))) - (lim (ProjMap1 ((Partial_Sums Rseq),m))))).| < e
( N >= N1 & N >= N2 ) by XXREAL_0:25;
then ( n >= N1 & n >= N2 ) by B9, XXREAL_0:2;
then ( |.(((ProjMap1 ((Partial_Sums Rseq),m)) . n) - (lim (ProjMap1 ((Partial_Sums Rseq),m)))).| < e / 2 & |.(((ProjMap1 ((Partial_Sums Rseq),k)) . n) - (lim (ProjMap1 ((Partial_Sums Rseq),k)))).| < e / 2 ) by B7, B8;
then B12: |.(((ProjMap1 ((Partial_Sums Rseq),m)) . n) - (lim (ProjMap1 ((Partial_Sums Rseq),m)))).| + |.(((ProjMap1 ((Partial_Sums Rseq),k)) . n) - (lim (ProjMap1 ((Partial_Sums Rseq),k)))).| < (e / 2) + (e / 2) by XREAL_1:8;
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
(ProjMap1 ((Partial_Sums Rseq),k)) . n = (Partial_Sums Rseq) . (k,n1) by MESFUNC9:def 6
.= (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . ((m + 1),n1) by B2, th103a
.= ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (m,n1)) + ((Partial_Sums_in_cod2 Rseq) . ((m + 1),n1)) by DefRS
.= ((Partial_Sums Rseq) . (m,n1)) + ((Partial_Sums_in_cod2 Rseq) . (k,n1)) by B2, th103a
.= ((ProjMap1 ((Partial_Sums Rseq),m)) . n) + ((Partial_Sums_in_cod2 Rseq) . (k,n1)) by MESFUNC9:def 6
.= ((ProjMap1 ((Partial_Sums Rseq),m)) . n) + ((ProjMap1 ((Partial_Sums_in_cod2 Rseq),k)) . n) by MESFUNC9:def 6 ;
then |.(((ProjMap1 ((Partial_Sums_in_cod2 Rseq),k)) . n) - ((lim (ProjMap1 ((Partial_Sums Rseq),k))) - (lim (ProjMap1 ((Partial_Sums Rseq),m))))).| = |.((((ProjMap1 ((Partial_Sums Rseq),k)) . n) - (lim (ProjMap1 ((Partial_Sums Rseq),k)))) - (((ProjMap1 ((Partial_Sums Rseq),m)) . n) - (lim (ProjMap1 ((Partial_Sums Rseq),m))))).| ;
then |.(((ProjMap1 ((Partial_Sums_in_cod2 Rseq),k)) . n) - ((lim (ProjMap1 ((Partial_Sums Rseq),k))) - (lim (ProjMap1 ((Partial_Sums Rseq),m))))).| <= |.(((ProjMap1 ((Partial_Sums Rseq),k)) . n) - (lim (ProjMap1 ((Partial_Sums Rseq),k)))).| + |.(((ProjMap1 ((Partial_Sums Rseq),m)) . n) - (lim (ProjMap1 ((Partial_Sums Rseq),m)))).| by COMPLEX1:57;
hence |.(((ProjMap1 ((Partial_Sums_in_cod2 Rseq),k)) . n) - ((lim (ProjMap1 ((Partial_Sums Rseq),k))) - (lim (ProjMap1 ((Partial_Sums Rseq),m))))).| < e by B12, XXREAL_0:2; :: thesis: verum

end;

end;

hence ProjMap1 ((Partial_Sums_in_cod2 Rseq),k) is convergent by SEQ_2:def 6; :: thesis: verum

end;

end;

for m1 being Nat holds S₁[m1] from NAT_1:sch 2(A3, A4);
hence ProjMap1 ((Partial_Sums_in_cod2 Rseq),m) is convergent ; :: thesis: verum

end;

hence Partial_Sums_in_cod2 Rseq is convergent_in_cod2 ; :: thesis: verum

end;

assume C0: Partial_Sums_in_cod2 Rseq is convergent_in_cod2 ; :: thesis: Partial_Sums Rseq is convergent_in_cod2

now :: thesis: for m being Element of NAT holds ProjMap1 ((Partial_Sums Rseq),m) is convergent

let m be Element of NAT ; :: thesis: ProjMap1 ((Partial_Sums Rseq),m) is convergent
defpred S₁[ Nat] means for k being Element of NAT st k = $1 holds
ProjMap1 ((Partial_Sums Rseq),k) is convergent ;
ProjMap1 ((Partial_Sums Rseq),0) = ProjMap1 ((Partial_Sums_in_cod2 Rseq),0) by th00;
then C1: S₁[ 0 ] by C0;
C2: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume C3: S₁[m] ; :: thesis: S₁[m + 1]
reconsider m1 = m as Element of NAT by ORDINAL1:def 12;

hereby :: thesis: verum

let k be Element of NAT ; :: thesis: ( k = m + 1 implies ProjMap1 ((Partial_Sums Rseq),k) is convergent )
assume C4: k = m + 1 ; :: thesis: ProjMap1 ((Partial_Sums Rseq),k) is convergent
then reconsider k1 = k - 1 as Element of NAT by NAT_1:11, NAT_1:21;
for n being Element of NAT holds (ProjMap1 ((Partial_Sums Rseq),k)) . n = ((ProjMap1 ((Partial_Sums Rseq),m1)) + (ProjMap1 ((Partial_Sums_in_cod2 Rseq),(m1 + 1)))) . n

proof

let n be Element of NAT ; :: thesis: (ProjMap1 ((Partial_Sums Rseq),k)) . n = ((ProjMap1 ((Partial_Sums Rseq),m1)) + (ProjMap1 ((Partial_Sums_in_cod2 Rseq),(m1 + 1)))) . n
(ProjMap1 ((Partial_Sums Rseq),k)) . n = (Partial_Sums Rseq) . ((m1 + 1),n) by C4, MESFUNC9:def 6
.= ((Partial_Sums_in_cod2 Rseq) . ((m1 + 1),n)) + ((Partial_Sums_in_cod2 (Partial_Sums_in_cod1 Rseq)) . (m1,n)) by ThRS
.= ((ProjMap1 ((Partial_Sums_in_cod2 Rseq),(m1 + 1))) . n) + ((Partial_Sums Rseq) . (m1,n)) by MESFUNC9:def 6
.= ((ProjMap1 ((Partial_Sums_in_cod2 Rseq),(m1 + 1))) . n) + ((ProjMap1 ((Partial_Sums Rseq),m1)) . n) by MESFUNC9:def 6 ;
hence (ProjMap1 ((Partial_Sums Rseq),k)) . n = ((ProjMap1 ((Partial_Sums Rseq),m1)) + (ProjMap1 ((Partial_Sums_in_cod2 Rseq),(m1 + 1)))) . n by VALUED_1:1; :: thesis: verum

end;

then C5: ProjMap1 ((Partial_Sums Rseq),k) = (ProjMap1 ((Partial_Sums Rseq),m1)) + (ProjMap1 ((Partial_Sums_in_cod2 Rseq),(m1 + 1))) ;
( ProjMap1 ((Partial_Sums Rseq),m1) is convergent & ProjMap1 ((Partial_Sums_in_cod2 Rseq),(m1 + 1)) is convergent ) by C3, C0;
hence ProjMap1 ((Partial_Sums Rseq),k) is convergent by C5, SEQ_2:5; :: thesis: verum

end;

end;

for m being Nat holds S₁[m] from NAT_1:sch 2(C1, C2);
hence ProjMap1 ((Partial_Sums Rseq),m) is convergent ; :: thesis: verum

end;

hence Partial_Sums Rseq is convergent_in_cod2 ; :: thesis: verum