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