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

now :: thesis: for K being Nat st ( for dseqK being Real_Sequence st ( for n being Nat holds dseqK . n = (Partial_Sums (cseq n)) . K ) holds
( dseqK is convergent & lim dseqK = (Partial_Sums eseq) . K ) ) holds
for dseqK1 being Real_Sequence st ( for n being Nat holds dseqK1 . n = (Partial_Sums (cseq n)) . (K + 1) ) holds
( dseqK1 is convergent & lim dseqK1 = (Partial_Sums eseq) . (K + 1) )

let K be Nat; :: thesis: ( ( for dseqK being Real_Sequence st ( for n being 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 Nat holds dseqK1 . n = (Partial_Sums (cseq n)) . (K + 1) ) holds
( dseqK1 is convergent & lim dseqK1 = (Partial_Sums eseq) . (K + 1) ) )
deffunc H₁( Nat) -> set = (Partial_Sums (cseq $1)) . K;
consider dseqK being Real_Sequence such that
A1: for n being Nat holds dseqK . n = H₁(n) from SEQ_1:sch 1();
assume A2: for dseqK being Real_Sequence st ( for n being 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 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 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 Nat holds dseqK1 . n = (Partial_Sums (cseq n)) . (K + 1) ; :: thesis: ( dseqK1 is convergent & lim dseqK1 = (Partial_Sums eseq) . (K + 1) )

now :: thesis: for n being Element of NAT holds dseqK1 . n = (dseqK + (bseq (K + 1))) . n

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:7 ; :: thesis: verum

end;

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

end;

then A8: for n being Nat st S₁[n] holds
S₁[n + 1] ;

now :: thesis: for dseq0 being Real_Sequence st ( for n being Nat holds dseq0 . n = (Partial_Sums (cseq n)) . 0 ) holds
( dseq0 is convergent & lim dseq0 = (Partial_Sums eseq) . 0 )

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

now :: thesis: for n being Element of NAT holds dseq0 . n = (bseq 0) . n

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:63;
hence dseq0 is convergent by Th12; :: thesis: lim dseq0 = (Partial_Sums eseq) . 0
thus lim dseq0 = eseq . 0 by A10, Th12
.= (Partial_Sums eseq) . 0 by SERIES_1:def 1 ; :: thesis: verum

end;

then A11: S₁[ 0 ] ;
thus for n being Nat holds S₁[n] from NAT_1:sch 2(A11, A8); :: thesis: verum