let Rseq be Function of [:NAT,NAT:],REAL; ( 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
; 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; (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 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)))) . jlet j be
Element of
NAT ;
(ProjMap2 ((Partial_Sums Rseq),(k1 + 1))) . j = ((ProjMap2 ((Partial_Sums Rseq),k1)) + (ProjMap2 ((Partial_Sums_in_cod1 Rseq),(k1 + 1)))) . jB1:
(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;
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; verum