let Rseq be Function of [:NAT,NAT:],REAL; :: thesis: ( Partial_Sums Rseq is convergent_in_cod1 implies for k being Nat holds (lim_in_cod1 (Partial_Sums Rseq)) . (k + 1) = ((lim_in_cod1 (Partial_Sums Rseq)) . k) + ((lim_in_cod1 (Partial_Sums_in_cod1 Rseq)) . (k + 1)) )
assume A1: Partial_Sums Rseq is convergent_in_cod1 ; :: thesis: for k being Nat holds (lim_in_cod1 (Partial_Sums Rseq)) . (k + 1) = ((lim_in_cod1 (Partial_Sums Rseq)) . k) + ((lim_in_cod1 (Partial_Sums_in_cod1 Rseq)) . (k + 1))
let k be Nat; :: thesis: (lim_in_cod1 (Partial_Sums Rseq)) . (k + 1) = ((lim_in_cod1 (Partial_Sums Rseq)) . k) + ((lim_in_cod1 (Partial_Sums_in_cod1 Rseq)) . (k + 1))
reconsider k1 = k as Element of NAT by ORDINAL1:def 12;
Partial_Sums_in_cod1 Rseq is convergent_in_cod1 by A1, th01a;
then A2: ( ProjMap2 ((Partial_Sums Rseq),k1) is convergent & ProjMap2 ((Partial_Sums_in_cod1 Rseq),(k1 + 1)) is convergent ) by A1;
A3: (lim_in_cod1 (Partial_Sums Rseq)) . (k + 1) = lim (ProjMap2 ((Partial_Sums Rseq),(k1 + 1))) by DBLSEQ_1:def 5;
A4: ( (lim_in_cod1 (Partial_Sums Rseq)) . k = lim (ProjMap2 ((Partial_Sums Rseq),k1)) & (lim_in_cod1 (Partial_Sums_in_cod1 Rseq)) . (k + 1) = lim (ProjMap2 ((Partial_Sums_in_cod1 Rseq),(k1 + 1))) ) by DBLSEQ_1:def 5;

now :: thesis: for j being Element of NAT holds (ProjMap2 ((Partial_Sums Rseq),(k1 + 1))) . j = ((ProjMap2 ((Partial_Sums Rseq),k1)) + (ProjMap2 ((Partial_Sums_in_cod1 Rseq),(k1 + 1)))) . j

let j be Element of NAT ; :: thesis: (ProjMap2 ((Partial_Sums Rseq),(k1 + 1))) . j = ((ProjMap2 ((Partial_Sums Rseq),k1)) + (ProjMap2 ((Partial_Sums_in_cod1 Rseq),(k1 + 1)))) . j
B1: (ProjMap2 ((Partial_Sums Rseq),k1)) . j = (Partial_Sums_in_cod2 (Partial_Sums_in_cod1 Rseq)) . (j,k1) by MESFUNC9:def 7;
(ProjMap2 ((Partial_Sums_in_cod1 Rseq),(k1 + 1))) . j = (Partial_Sums_in_cod1 Rseq) . (j,(k1 + 1)) by MESFUNC9:def 7;
then ((ProjMap2 ((Partial_Sums Rseq),k1)) . j) + ((ProjMap2 ((Partial_Sums_in_cod1 Rseq),(k1 + 1))) . j) = (Partial_Sums_in_cod2 (Partial_Sums_in_cod1 Rseq)) . (j,(k1 + 1)) by B1, DefCS
.= (ProjMap2 ((Partial_Sums Rseq),(k1 + 1))) . j by MESFUNC9:def 7 ;
hence (ProjMap2 ((Partial_Sums Rseq),(k1 + 1))) . j = ((ProjMap2 ((Partial_Sums Rseq),k1)) + (ProjMap2 ((Partial_Sums_in_cod1 Rseq),(k1 + 1)))) . j by VALUED_1:1; :: thesis: verum

end;

then ProjMap2 ((Partial_Sums Rseq),(k1 + 1)) = (ProjMap2 ((Partial_Sums Rseq),k1)) + (ProjMap2 ((Partial_Sums_in_cod1 Rseq),(k1 + 1))) ;
hence (lim_in_cod1 (Partial_Sums Rseq)) . (k + 1) = ((lim_in_cod1 (Partial_Sums Rseq)) . k) + ((lim_in_cod1 (Partial_Sums_in_cod1 Rseq)) . (k + 1)) by A3, A4, A2, SEQ_2:6; :: thesis: verum