defpred S₁[ Element of NAT ] means for dseqK being Real_Sequence st ( for n being Element of NAT holds dseqK . n = (Partial_Sums (cseq n)) . $1 ) holds
( dseqK is convergent & lim dseqK = (Partial_Sums eseq ) . $1 );

now

let K be Element of NAT ; :: thesis: ( ( for dseqK being Real_Sequence st ( for n being Element of NAT holds dseqK . n = (Partial_Sums (cseq n)) . K ) holds
( dseqK is convergent & lim dseqK = (Partial_Sums eseq ) . K ) ) implies for dseqK1 being Real_Sequence st ( for n being Element of NAT holds dseqK1 . n = (Partial_Sums (cseq n)) . (K + 1) ) holds
( dseqK1 is convergent & lim dseqK1 = (Partial_Sums eseq ) . (K + 1) ) )
deffunc H₁( Element of NAT ) -> Element of REAL = (Partial_Sums (cseq $1)) . K;
consider dseqK being Real_Sequence such that
A1: for n being Element of NAT holds dseqK . n = H₁(n) from SEQ_1:sch 1();
assume A2: for dseqK being Real_Sequence st ( for n being Element of NAT holds dseqK . n = (Partial_Sums (cseq n)) . K ) holds
( dseqK is convergent & lim dseqK = (Partial_Sums eseq ) . K ) ; :: thesis: for dseqK1 being Real_Sequence st ( for n being Element of NAT holds dseqK1 . n = (Partial_Sums (cseq n)) . (K + 1) ) holds
( dseqK1 is convergent & lim dseqK1 = (Partial_Sums eseq ) . (K + 1) )
then A3: dseqK is convergent by A1;
let dseqK1 be Real_Sequence; :: thesis: ( ( for n being Element of NAT holds dseqK1 . n = (Partial_Sums (cseq n)) . (K + 1) ) implies ( dseqK1 is convergent & lim dseqK1 = (Partial_Sums eseq ) . (K + 1) ) )
assume A4: for n being Element of NAT holds dseqK1 . n = (Partial_Sums (cseq n)) . (K + 1) ; :: thesis: ( dseqK1 is convergent & lim dseqK1 = (Partial_Sums eseq ) . (K + 1) )

now

let n be Element of NAT ; :: thesis: dseqK1 . n = (dseqK + (bseq (K + 1))) . n
thus dseqK1 . n = (Partial_Sums (cseq n)) . (K + 1) by A4
.= ((Partial_Sums (cseq n)) . K) + ((cseq n) . (K + 1)) by SERIES_1:def 1
.= (dseqK . n) + ((cseq n) . (K + 1)) by A1
.= (dseqK . n) + ((bseq (K + 1)) . n) by Th3
.= (dseqK + (bseq (K + 1))) . n by SEQ_1:11 ; :: thesis: verum

end;

then A5: dseqK1 = dseqK + (bseq (K + 1)) by FUNCT_2:113;
A6: lim dseqK = (Partial_Sums eseq ) . K by A2, A1;
A7: bseq (K + 1) is convergent by Th13;
hence dseqK1 is convergent by A3, A5, SEQ_2:19; :: thesis: lim dseqK1 = (Partial_Sums eseq ) . (K + 1)
thus lim dseqK1 = (lim dseqK) + (lim (bseq (K + 1))) by A3, A5, A7, SEQ_2:20
.= ((Partial_Sums eseq ) . K) + (eseq . (K + 1)) by A6, Th13
.= (Partial_Sums eseq ) . (K + 1) by SERIES_1:def 1 ; :: thesis: verum

end;

then A8: for n being Element of NAT st S₁[n] holds
S₁[n + 1] ;

now

let dseq0 be Real_Sequence; :: thesis: ( ( for n being Element of NAT holds dseq0 . n = (Partial_Sums (cseq n)) . 0 ) implies ( dseq0 is convergent & lim dseq0 = (Partial_Sums eseq ) . 0 ) )
assume A9: for n being Element of NAT holds dseq0 . n = (Partial_Sums (cseq n)) . 0 ; :: thesis: ( dseq0 is convergent & lim dseq0 = (Partial_Sums eseq ) . 0 )

now

let n be Element of NAT ; :: thesis: dseq0 . n = (bseq 0 ) . n
thus dseq0 . n = (Partial_Sums (cseq n)) . 0 by A9
.= (cseq n) . 0 by SERIES_1:def 1
.= (bseq 0 ) . n by Th3 ; :: thesis: verum

end;

then A10: dseq0 = bseq 0 by FUNCT_2:113;
hence dseq0 is convergent by Th13; :: thesis: lim dseq0 = (Partial_Sums eseq ) . 0
thus lim dseq0 = eseq . 0 by A10, Th13
.= (Partial_Sums eseq ) . 0 by SERIES_1:def 1 ; :: thesis: verum

end;

then A11: S₁[ 0 ] ;
thus for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A11, A8); :: thesis: verum