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

hereby :: thesis: ( Partial_Sums_in_cod1 Rseq is convergent_in_cod1 implies Partial_Sums Rseq is convergent_in_cod1 )

assume A1: Partial_Sums Rseq is convergent_in_cod1 ; :: thesis: Partial_Sums_in_cod1 Rseq is convergent_in_cod1

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

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

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

let k be Element of NAT ; :: thesis: ( k = 0 implies ProjMap2 ((Partial_Sums_in_cod1 Rseq),k) is convergent )
assume k = 0 ; :: thesis: ProjMap2 ((Partial_Sums_in_cod1 Rseq),k) is convergent
then ProjMap2 ((Partial_Sums Rseq),k) = ProjMap2 ((Partial_Sums_in_cod1 Rseq),k) by th00;
hence ProjMap2 ((Partial_Sums_in_cod1 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 ProjMap2 ((Partial_Sums_in_cod1 Rseq),k) is convergent )
assume B2: k = m1 + 1 ; :: thesis: ProjMap2 ((Partial_Sums_in_cod1 Rseq),k) is convergent
then reconsider k1 = k - 1 as Element of NAT by NAT_1:11, NAT_1:21;
B4: ( ProjMap2 ((Partial_Sums Rseq),m) is convergent & ProjMap2 ((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
|.(((ProjMap2 ((Partial_Sums_in_cod1 Rseq),k)) . n) - ((lim (ProjMap2 ((Partial_Sums Rseq),k))) - (lim (ProjMap2 ((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
|.(((ProjMap2 ((Partial_Sums_in_cod1 Rseq),k)) . n) - ((lim (ProjMap2 ((Partial_Sums Rseq),k))) - (lim (ProjMap2 ((Partial_Sums Rseq),m))))).| < e )
assume B6: 0 < e ; :: thesis: ex N being Nat st
for n being Nat st n >= N holds
|.(((ProjMap2 ((Partial_Sums_in_cod1 Rseq),k)) . n) - ((lim (ProjMap2 ((Partial_Sums Rseq),k))) - (lim (ProjMap2 ((Partial_Sums Rseq),m))))).| < e
then consider N1 being Nat such that
B7: for n being Nat st n >= N1 holds
|.(((ProjMap2 ((Partial_Sums Rseq),m)) . n) - (lim (ProjMap2 ((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
|.(((ProjMap2 ((Partial_Sums Rseq),k)) . n) - (lim (ProjMap2 ((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
|.(((ProjMap2 ((Partial_Sums_in_cod1 Rseq),k)) . n) - ((lim (ProjMap2 ((Partial_Sums Rseq),k))) - (lim (ProjMap2 ((Partial_Sums Rseq),m))))).| < e

hereby :: thesis: verum

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

end;

end;

hence ProjMap2 ((Partial_Sums_in_cod1 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 ProjMap2 ((Partial_Sums_in_cod1 Rseq),m) is convergent ; :: thesis: verum

end;

hence Partial_Sums_in_cod1 Rseq is convergent_in_cod1 ; :: thesis: verum

end;

assume C0: Partial_Sums_in_cod1 Rseq is convergent_in_cod1 ; :: thesis: Partial_Sums Rseq is convergent_in_cod1

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

let m be Element of NAT ; :: thesis: ProjMap2 ((Partial_Sums Rseq),m) is convergent
defpred S₁[ Nat] means for k being Element of NAT st k = $1 holds
ProjMap2 ((Partial_Sums Rseq),k) is convergent ;
ProjMap2 ((Partial_Sums Rseq),0) = ProjMap2 ((Partial_Sums_in_cod1 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 ProjMap2 ((Partial_Sums Rseq),k) is convergent )
assume C4: k = m + 1 ; :: thesis: ProjMap2 ((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 (ProjMap2 ((Partial_Sums Rseq),k)) . n = ((ProjMap2 ((Partial_Sums Rseq),m1)) + (ProjMap2 ((Partial_Sums_in_cod1 Rseq),(m1 + 1)))) . n

proof

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

end;

then C5: ProjMap2 ((Partial_Sums Rseq),k) = (ProjMap2 ((Partial_Sums Rseq),m1)) + (ProjMap2 ((Partial_Sums_in_cod1 Rseq),(m1 + 1))) ;
( ProjMap2 ((Partial_Sums Rseq),m1) is convergent & ProjMap2 ((Partial_Sums_in_cod1 Rseq),(m1 + 1)) is convergent ) by C3, C0;
hence ProjMap2 ((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 ProjMap2 ((Partial_Sums Rseq),m) is convergent ; :: thesis: verum

end;

hence Partial_Sums Rseq is convergent_in_cod1 ; :: thesis: verum