let f be without-infty Function of [:NAT,NAT:],ExtREAL; :: thesis:

assume A1: Partial_Sums f is convergent_in_cod1_to_finite ; :: thesis:

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

now :: thesis:

let k be Element of NAT ; :: thesis:
assume k = 0 ; :: thesis:
then ProjMap2 ((Partial_Sums f),k) = ProjMap2 ((Partial_Sums_in_cod1 f),k) by Th54;
hence ProjMap2 ((Partial_Sums_in_cod1 f),k) is convergent_to_finite_number by A1; :: thesis:

end;

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

proof

let m1 be Nat; :: thesis:
reconsider m = m1 as Element of NAT by ORDINAL1:def 12;
assume X1: S₁[m1] ; :: thesis:

hereby :: thesis:

let k be Element of NAT ; :: thesis:
assume B2: k = m1 + 1 ; :: thesis:
then reconsider k1 = k - 1 as Element of NAT by NAT_1:11, NAT_1:21;
F1: ProjMap2 ((Partial_Sums_in_cod1 f),m) is convergent_to_finite_number by X1;
( not ProjMap2 ((Partial_Sums_in_cod1 f),m) is convergent_to_+infty & not ProjMap2 ((Partial_Sums_in_cod1 f),m) is convergent_to_-infty ) by X1, MESFUNC5:50, MESFUNC5:51;
then consider G0 being Real such that
F3: ( lim (ProjMap2 ((Partial_Sums_in_cod1 f),m)) = G0 & ( 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 f),m)) . n) - (lim (ProjMap2 ((Partial_Sums_in_cod1 f),m)))).| < e ) & ProjMap2 ((Partial_Sums_in_cod1 f),m) is convergent_to_finite_number ) by F1, MESFUNC5:def 12;
consider G1 being Real such that
E3: ( lim (ProjMap2 ((Partial_Sums f),m)) = G1 & ( for e being Real st 0 < e holds
ex N being Nat st
for n being Nat st N <= n holds
|.(((ProjMap2 ((Partial_Sums f),m)) . n) - (lim (ProjMap2 ((Partial_Sums f),m)))).| < e ) ) by A1, MESFUNC9:7;
consider G2 being Real such that
E4: ( lim (ProjMap2 ((Partial_Sums f),k)) = G2 & ( for e being Real st 0 < e holds
ex N being Nat st
for n being Nat st N <= n holds
|.(((ProjMap2 ((Partial_Sums f),k)) . n) - (lim (ProjMap2 ((Partial_Sums f),k)))).| < e ) ) by A1, MESFUNC9:7;
E7: ( - G1 = - (lim (ProjMap2 ((Partial_Sums f),m))) & - G2 = - (lim (ProjMap2 ((Partial_Sums f),k))) ) by E3, E4, XXREAL_3:def 3;
then E5: G2 + (- G1) = (lim (ProjMap2 ((Partial_Sums f),k))) + (- (lim (ProjMap2 ((Partial_Sums f),m)))) by E4, XXREAL_3:def 2;

now :: thesis:

let e be Real; :: thesis:
assume B6: 0 < e ; :: thesis:
then consider N1 being Nat such that
B7: for n being Nat st n >= N1 holds
|.(((ProjMap2 ((Partial_Sums f),m)) . n) - (lim (ProjMap2 ((Partial_Sums f),m)))).| < e / 2 by E3;
consider N2 being Nat such that
B8: for n being Nat st n >= N2 holds
|.(((ProjMap2 ((Partial_Sums f),k)) . n) - (lim (ProjMap2 ((Partial_Sums f),k)))).| < e / 2 by B6, E4;
consider N0 being Nat such that
B10: for n being Nat st n >= N0 holds
|.(((ProjMap2 ((Partial_Sums_in_cod1 f),m)) . n) - (lim (ProjMap2 ((Partial_Sums_in_cod1 f),m)))).| < e by B6, F3;
reconsider N = max ((max (N1,N2)),N0) as Nat by TARSKI:1;
take N = N; :: thesis:

hereby :: thesis:

K2: now :: thesis:

assume (ProjMap2 ((Partial_Sums f),m)) . n = +infty ; :: thesis:
then ((ProjMap2 ((Partial_Sums f),m)) . n) - (lim (ProjMap2 ((Partial_Sums f),m))) = +infty by E3, XXREAL_3:13;
hence contradiction by K0, B7, XXREAL_0:3, EXTREAL1:30; :: thesis:

end;

KK2: now :: thesis:

assume (ProjMap2 ((Partial_Sums f),m)) . n = -infty ; :: thesis:
then ((ProjMap2 ((Partial_Sums f),m)) . n) - (lim (ProjMap2 ((Partial_Sums f),m))) = -infty by E3, XXREAL_3:14;
hence contradiction by K0, B7, XXREAL_0:3, EXTREAL1:30; :: thesis:

end;

K5: now :: thesis:

assume (ProjMap2 ((Partial_Sums f),k)) . n = +infty ; :: thesis:
then ((ProjMap2 ((Partial_Sums f),k)) . n) - (lim (ProjMap2 ((Partial_Sums f),k))) = +infty by E4, XXREAL_3:13;
hence contradiction by K0, B8, XXREAL_0:3, EXTREAL1:30; :: thesis:

end;

KK5: now :: thesis:

assume (ProjMap2 ((Partial_Sums f),k)) . n = -infty ; :: thesis:
then ((ProjMap2 ((Partial_Sums f),k)) . n) - (lim (ProjMap2 ((Partial_Sums f),k))) = -infty by E4, XXREAL_3:14;
hence contradiction by K0, B8, XXREAL_0:3, EXTREAL1:30; :: thesis:

end;

end;

hence ProjMap2 ((Partial_Sums_in_cod1 f),k) is convergent_to_finite_number by MESFUNC5:def 8; :: thesis:

end;

for m1 being Nat holds S₁[m1] from NAT_1:sch 2(A3, A4);
hence ProjMap2 ((Partial_Sums_in_cod1 f),m) is convergent_to_finite_number ; :: thesis:

end;

hence Partial_Sums_in_cod1 f is convergent_in_cod1_to_finite ; :: thesis:

end;

assume C0: Partial_Sums_in_cod1 f is convergent_in_cod1_to_finite ; :: thesis:

now :: thesis:

let m be Element of NAT ; :: thesis:
defpred S₁[ Nat] means for k being Element of NAT st k = $1 holds
ProjMap2 ((Partial_Sums f),k) is convergent_to_finite_number ;
ProjMap2 ((Partial_Sums f),0) = ProjMap2 ((Partial_Sums_in_cod1 f),0) by Th54;
then C1: S₁[ 0 ] by C0;
C2: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

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

hereby :: thesis:

let k be Element of NAT ; :: thesis:
assume C4: k = m + 1 ; :: thesis:
then reconsider k1 = k - 1 as Element of NAT by NAT_1:11, NAT_1:21;
reconsider f1 = ProjMap2 ((Partial_Sums f),m1), f2 = ProjMap2 ((Partial_Sums_in_cod1 f),(m1 + 1)) as without-infty ExtREAL_sequence ;
for n being Element of NAT holds (ProjMap2 ((Partial_Sums f),k)) . n = ((ProjMap2 ((Partial_Sums f),m1)) + (ProjMap2 ((Partial_Sums_in_cod1 f),(m1 + 1)))) . n

proof

end;

then C5: ProjMap2 ((Partial_Sums f),k) = f1 + f2 by FUNCT_2:def 8;
( ProjMap2 ((Partial_Sums f),m1) is convergent_to_finite_number & ProjMap2 ((Partial_Sums_in_cod1 f),(m1 + 1)) is convergent_to_finite_number ) by C3, C0;
hence ProjMap2 ((Partial_Sums f),k) is convergent_to_finite_number by C5, Th23; :: thesis:

end;

for m being Nat holds S₁[m] from NAT_1:sch 2(C1, C2);
hence ProjMap2 ((Partial_Sums f),m) is convergent_to_finite_number ; :: thesis:

end;

hence Partial_Sums f is convergent_in_cod1_to_finite ; :: thesis: