let Rseq be Function of [:NAT,NAT:],REAL; :: thesis: ( Partial_Sums Rseq is convergent_in_cod2 implies for k being Nat holds (lim_in_cod2 (Partial_Sums Rseq)) . (k + 1) = ((lim_in_cod2 (Partial_Sums Rseq)) . k) + ((lim_in_cod2 (Partial_Sums_in_cod2 Rseq)) . (k + 1)) )
assume A1: Partial_Sums Rseq is convergent_in_cod2 ; :: thesis: for k being Nat holds (lim_in_cod2 (Partial_Sums Rseq)) . (k + 1) = ((lim_in_cod2 (Partial_Sums Rseq)) . k) + ((lim_in_cod2 (Partial_Sums_in_cod2 Rseq)) . (k + 1))
let k be Nat; :: thesis: (lim_in_cod2 (Partial_Sums Rseq)) . (k + 1) = ((lim_in_cod2 (Partial_Sums Rseq)) . k) + ((lim_in_cod2 (Partial_Sums_in_cod2 Rseq)) . (k + 1))
reconsider k1 = k as Element of NAT by ORDINAL1:def 12;
Partial_Sums_in_cod2 Rseq is convergent_in_cod2 by A1, th01b;
then A2: ( ProjMap1 ((Partial_Sums Rseq),k1) is convergent & ProjMap1 ((Partial_Sums_in_cod2 Rseq),(k1 + 1)) is convergent ) by A1;
A3: (lim_in_cod2 (Partial_Sums Rseq)) . (k + 1) = lim (ProjMap1 ((Partial_Sums Rseq),(k1 + 1))) by DBLSEQ_1:def 6;
A4: ( (lim_in_cod2 (Partial_Sums Rseq)) . k = lim (ProjMap1 ((Partial_Sums Rseq),k1)) & (lim_in_cod2 (Partial_Sums_in_cod2 Rseq)) . (k + 1) = lim (ProjMap1 ((Partial_Sums_in_cod2 Rseq),(k1 + 1))) ) by DBLSEQ_1:def 6;

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

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

end;

then ProjMap1 ((Partial_Sums Rseq),(k1 + 1)) = (ProjMap1 ((Partial_Sums Rseq),k1)) + (ProjMap1 ((Partial_Sums_in_cod2 Rseq),(k1 + 1))) ;
hence (lim_in_cod2 (Partial_Sums Rseq)) . (k + 1) = ((lim_in_cod2 (Partial_Sums Rseq)) . k) + ((lim_in_cod2 (Partial_Sums_in_cod2 Rseq)) . (k + 1)) by A3, A4, A2, SEQ_2:6; :: thesis: verum