let f be nonnegative Function of [:NAT,NAT:],ExtREAL; :: thesis: ( Partial_Sums f is convergent_in_cod1_to_finite implies for m being Element of NAT holds (Partial_Sums (lim_in_cod1 (Partial_Sums_in_cod1 f))) . m = lim (ProjMap2 ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)),m)) )
assume A1: Partial_Sums f is convergent_in_cod1_to_finite ; :: thesis: for m being Element of NAT holds (Partial_Sums (lim_in_cod1 (Partial_Sums_in_cod1 f))) . m = lim (ProjMap2 ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)),m))
then A2: Partial_Sums_in_cod1 f is convergent_in_cod1_to_finite by Th79;
let m be Element of NAT ; :: thesis: (Partial_Sums (lim_in_cod1 (Partial_Sums_in_cod1 f))) . m = lim (ProjMap2 ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)),m))
defpred S₁[ Nat] means for k being Element of NAT st k <= $1 holds
(Partial_Sums (lim_in_cod1 (Partial_Sums_in_cod1 f))) . k = lim (ProjMap2 ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)),k));

now :: thesis: for k being Element of NAT st k <= 0 holds
(Partial_Sums (lim_in_cod1 (Partial_Sums_in_cod1 f))) . k = lim (ProjMap2 ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)),k))

let k be Element of NAT ; :: thesis: ( k <= 0 implies (Partial_Sums (lim_in_cod1 (Partial_Sums_in_cod1 f))) . k = lim (ProjMap2 ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)),k)) )
assume k <= 0 ; :: thesis: (Partial_Sums (lim_in_cod1 (Partial_Sums_in_cod1 f))) . k = lim (ProjMap2 ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)),k))
then A5: k = 0 ;
A6: (Partial_Sums (lim_in_cod1 (Partial_Sums_in_cod1 f))) . 0 = (lim_in_cod1 (Partial_Sums_in_cod1 f)) . 0 by MESFUNC9:def 1
.= lim (ProjMap2 ((Partial_Sums_in_cod1 f),0)) by D1DEF5 ;
consider G being Real such that
A7: ( lim (ProjMap2 ((Partial_Sums_in_cod1 f),0)) = G & ( for p being Real st 0 < p holds
ex N being Nat st
for n being Nat st N <= n holds
|.(((ProjMap2 ((Partial_Sums_in_cod1 f),0)) . n) - (lim (ProjMap2 ((Partial_Sums_in_cod1 f),0)))).| < p ) ) by A2, MESFUNC9:7;
reconsider G1 = G as R_eal by XXREAL_0:def 1;
ProjMap2 ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)),0) = ProjMap2 ((Partial_Sums f),0) by Lm8;
then A8: ProjMap2 ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)),0) is convergent_to_finite_number by A1;
for p being Real st 0 < p holds
ex N being Nat st
for n being Nat st N <= n holds
|.(((ProjMap2 ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)),0)) . n) - G1).| < p

proof

let p be Real; :: thesis: ( 0 < p implies ex N being Nat st
for n being Nat st N <= n holds
|.(((ProjMap2 ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)),0)) . n) - G1).| < p )
assume 0 < p ; :: thesis: ex N being Nat st
for n being Nat st N <= n holds
|.(((ProjMap2 ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)),0)) . n) - G1).| < p
then consider N being Nat such that
A11: for n being Nat st N <= n holds
|.(((ProjMap2 ((Partial_Sums_in_cod1 f),0)) . n) - G1).| < p by A7;

now :: thesis: for n being Nat st N <= n holds
|.(((ProjMap2 ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)),0)) . n) - G1).| < p

let n be Nat; :: thesis: ( N <= n implies |.(((ProjMap2 ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)),0)) . n) - G1).| < p )
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
assume A12: N <= n ; :: thesis: |.(((ProjMap2 ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)),0)) . n) - G1).| < p
(ProjMap2 ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)),0)) . n1 = (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (n,0) by MESFUNC9:def 7
.= (Partial_Sums f) . (n,0) by Lm8
.= (ProjMap2 ((Partial_Sums f),0)) . n1 by MESFUNC9:def 7
.= (ProjMap2 ((Partial_Sums_in_cod1 f),0)) . n1 by Th54 ;
hence |.(((ProjMap2 ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)),0)) . n) - G1).| < p by A11, A12; :: thesis: verum

end;

hence ex N being Nat st
for n being Nat st N <= n holds
|.(((ProjMap2 ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)),0)) . n) - G1).| < p ; :: thesis: verum

end;

hence (Partial_Sums (lim_in_cod1 (Partial_Sums_in_cod1 f))) . k = lim (ProjMap2 ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)),k)) by A5, A6, A7, A8, MESFUNC5:def 12; :: thesis: verum

end;

then A13: S₁[ 0 ] ;
A14: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

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

now :: thesis: for k being Element of NAT st k <= n + 1 holds
(Partial_Sums (lim_in_cod1 (Partial_Sums_in_cod1 f))) . k = lim (ProjMap2 ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)),k))

let k be Element of NAT ; :: thesis: ( k <= n + 1 implies (Partial_Sums (lim_in_cod1 (Partial_Sums_in_cod1 f))) . b₁ = lim (ProjMap2 ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)),b₁)) )
assume A16: k <= n + 1 ; :: thesis: (Partial_Sums (lim_in_cod1 (Partial_Sums_in_cod1 f))) . b₁ = lim (ProjMap2 ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)),b₁))

per cases ( k < n + 1 or k >= n + 1 ) ;

suppose k < n + 1 ; :: thesis: (Partial_Sums (lim_in_cod1 (Partial_Sums_in_cod1 f))) . b₁ = lim (ProjMap2 ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)),b₁))

then k <= n by NAT_1:13;
hence (Partial_Sums (lim_in_cod1 (Partial_Sums_in_cod1 f))) . k = lim (ProjMap2 ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)),k)) by A15; :: thesis: verum

end;

suppose k >= n + 1 ; :: thesis: (Partial_Sums (lim_in_cod1 (Partial_Sums_in_cod1 f))) . b₁ = lim (ProjMap2 ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)),b₁))

then A17: k = n + 1 by A16, XXREAL_0:1;
then A18: (Partial_Sums (lim_in_cod1 (Partial_Sums_in_cod1 f))) . k = ((Partial_Sums (lim_in_cod1 (Partial_Sums_in_cod1 f))) . n) + ((lim_in_cod1 (Partial_Sums_in_cod1 f)) . (n + 1)) by MESFUNC9:def 1
.= (lim (ProjMap2 ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)),n1))) + ((lim_in_cod1 (Partial_Sums_in_cod1 f)) . (n + 1)) by A15
.= (lim (ProjMap2 ((Partial_Sums f),n1))) + ((lim_in_cod1 (Partial_Sums_in_cod1 f)) . (n + 1)) by Lm8
.= (lim (ProjMap2 ((Partial_Sums f),n1))) + (lim (ProjMap2 ((Partial_Sums_in_cod1 f),k))) by A17, D1DEF5 ;
consider Gn being Real such that
A19: ( lim (ProjMap2 ((Partial_Sums f),n1)) = Gn & ( for p being Real st 0 < p holds
ex I being Nat st
for i being Nat st I <= i holds
|.(((ProjMap2 ((Partial_Sums f),n1)) . i) - (lim (ProjMap2 ((Partial_Sums f),n1)))).| < p ) ) by A1, MESFUNC9:7;
consider Gn1 being Real such that
A20: ( lim (ProjMap2 ((Partial_Sums_in_cod1 f),k)) = Gn1 & ( for p being Real st 0 < p holds
ex I being Nat st
for i being Nat st I <= i holds
|.(((ProjMap2 ((Partial_Sums_in_cod1 f),k)) . i) - (lim (ProjMap2 ((Partial_Sums_in_cod1 f),k)))).| < p ) ) by A2, MESFUNC9:7;
reconsider Gna = Gn, Gn1a = Gn1 as R_eal by XXREAL_0:def 1;
set G = Gna + Gn1a;
A21: lim (ProjMap2 ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)),k)) = (lim_in_cod1 (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f))) . k by D1DEF5
.= (lim_in_cod1 (Partial_Sums f)) . k by Lm8
.= lim (ProjMap2 ((Partial_Sums f),k)) by D1DEF5 ;
A22: ProjMap2 ((Partial_Sums f),k) is convergent_to_finite_number by A1;
for p being Real st 0 < p holds
ex I being Nat st
for i being Nat st I <= i holds
|.(((ProjMap2 ((Partial_Sums f),k)) . i) - (Gna + Gn1a)).| < p

proof

let p be Real; :: thesis: ( 0 < p implies ex I being Nat st
for i being Nat st I <= i holds
|.(((ProjMap2 ((Partial_Sums f),k)) . i) - (Gna + Gn1a)).| < p )
assume A24: 0 < p ; :: thesis: ex I being Nat st
for i being Nat st I <= i holds
|.(((ProjMap2 ((Partial_Sums f),k)) . i) - (Gna + Gn1a)).| < p
then consider I1 being Nat such that
A25: for i being Nat st I1 <= i holds
|.(((ProjMap2 ((Partial_Sums f),n1)) . i) - (lim (ProjMap2 ((Partial_Sums f),n1)))).| < p / 2 by A19;
consider I2 being Nat such that
A26: for i being Nat st I2 <= i holds
|.(((ProjMap2 ((Partial_Sums_in_cod1 f),k)) . i) - (lim (ProjMap2 ((Partial_Sums_in_cod1 f),k)))).| < p / 2 by A20, A24;
reconsider I = max (I1,I2) as Nat by XXREAL_0:16;
A27: ( I >= I1 & I >= I2 ) by XXREAL_0:25;

now :: thesis: for i being Nat st I <= i holds
|.(((ProjMap2 ((Partial_Sums f),k)) . i) - (Gna + Gn1a)).| < p

let i be Nat; :: thesis: ( I <= i implies |.(((ProjMap2 ((Partial_Sums f),k)) . i) - (Gna + Gn1a)).| < p )
reconsider i1 = i as Element of NAT by ORDINAL1:def 12;
assume I <= i ; :: thesis: |.(((ProjMap2 ((Partial_Sums f),k)) . i) - (Gna + Gn1a)).| < p
then ( I1 <= i & I2 <= i ) by A27, XXREAL_0:2;
then ( |.(((ProjMap2 ((Partial_Sums f),n1)) . i) - Gn).| < p / 2 & |.(((ProjMap2 ((Partial_Sums_in_cod1 f),k)) . i) - Gn1).| < p / 2 ) by A19, A20, A25, A26;
then A28: |.(((ProjMap2 ((Partial_Sums f),n1)) . i) - Gn).| + |.(((ProjMap2 ((Partial_Sums_in_cod1 f),k)) . i) - Gn1).| < (p / 2) + (p / 2) by XXREAL_3:64;
A29: (ProjMap2 ((Partial_Sums f),k)) . i1 = (Partial_Sums f) . (i,k) by MESFUNC9:def 7
.= (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (i,k) by Lm8
.= ((Partial_Sums_in_cod1 f) . (i,k)) + ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (i,n)) by A17, Th47
.= ((Partial_Sums f) . (i,n)) + ((Partial_Sums_in_cod1 f) . (i,k)) by Lm8
.= ((ProjMap2 ((Partial_Sums f),n1)) . i1) + ((Partial_Sums_in_cod1 f) . (i,k)) by MESFUNC9:def 7
.= ((ProjMap2 ((Partial_Sums f),n1)) . i1) + ((ProjMap2 ((Partial_Sums_in_cod1 f),k)) . i1) by MESFUNC9:def 7 ;
(ProjMap2 ((Partial_Sums_in_cod1 f),k)) . i1 <> -infty by SUPINF_2:51;
then A30: ((ProjMap2 ((Partial_Sums_in_cod1 f),k)) . i1) - Gn1a <> -infty by XXREAL_3:19;
then A31: (((ProjMap2 ((Partial_Sums_in_cod1 f),k)) . i1) - Gn1a) + Gn1a <> -infty by XXREAL_3:17;
(ProjMap2 ((Partial_Sums f),n1)) . i1 >= 0 by SUPINF_2:51;
then A32: ((ProjMap2 ((Partial_Sums f),n1)) . i) - Gna <> -infty by XXREAL_3:19;
( (ProjMap2 ((Partial_Sums f),n1)) . i = (((ProjMap2 ((Partial_Sums f),n1)) . i) - Gna) + Gna & (ProjMap2 ((Partial_Sums_in_cod1 f),k)) . i = (((ProjMap2 ((Partial_Sums_in_cod1 f),k)) . i) - Gn1a) + Gn1a ) by XXREAL_3:22;
then (ProjMap2 ((Partial_Sums f),k)) . i = (((ProjMap2 ((Partial_Sums f),n1)) . i) - Gna) + (((((ProjMap2 ((Partial_Sums_in_cod1 f),k)) . i) - Gn1a) + Gn1a) + Gna) by A29, A31, A32, XXREAL_3:29
.= (((ProjMap2 ((Partial_Sums f),n1)) . i) - Gna) + ((((ProjMap2 ((Partial_Sums_in_cod1 f),k)) . i) - Gn1a) + (Gn1a + Gna)) by XXREAL_3:29
.= ((((ProjMap2 ((Partial_Sums f),n1)) . i) - Gna) + (((ProjMap2 ((Partial_Sums_in_cod1 f),k)) . i) - Gn1a)) + (Gna + Gn1a) by A30, A32, XXREAL_3:29 ;
then ((ProjMap2 ((Partial_Sums f),k)) . i) - (Gna + Gn1a) = (((ProjMap2 ((Partial_Sums f),n1)) . i) - Gna) + (((ProjMap2 ((Partial_Sums_in_cod1 f),k)) . i) - Gn1a) by XXREAL_3:22;
then |.(((ProjMap2 ((Partial_Sums f),k)) . i) - (Gna + Gn1a)).| <= |.(((ProjMap2 ((Partial_Sums f),n1)) . i) - Gna).| + |.(((ProjMap2 ((Partial_Sums_in_cod1 f),k)) . i) - Gn1a).| by EXTREAL1:24;
hence |.(((ProjMap2 ((Partial_Sums f),k)) . i) - (Gna + Gn1a)).| < p by A28, XXREAL_0:2; :: thesis: verum

end;

hence ex I being Nat st
for i being Nat st I <= i holds
|.(((ProjMap2 ((Partial_Sums f),k)) . i) - (Gna + Gn1a)).| < p ; :: thesis: verum

end;

hence (Partial_Sums (lim_in_cod1 (Partial_Sums_in_cod1 f))) . k = lim (ProjMap2 ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)),k)) by A18, A19, A20, A21, A22, MESFUNC5:def 12; :: thesis: verum

end;

end;

end;

hence S₁[n + 1] ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A13, A14);
hence (Partial_Sums (lim_in_cod1 (Partial_Sums_in_cod1 f))) . m = lim (ProjMap2 ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)),m)) ; :: thesis: verum