defpred S1[ 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 = . \$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 = . 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 = . (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 = . 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 = . (K + 1) ) )

deffunc H1( Nat) -> set = (Partial_Sums (cseq \$1)) . K;
consider dseqK being Real_Sequence such that
A1: for n being Nat holds dseqK . n = H1(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 = . 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 = . (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 = . (K + 1) ) )
assume A4: for n being Nat holds dseqK1 . n = (Partial_Sums (cseq n)) . (K + 1) ; :: thesis: ( dseqK1 is convergent & lim dseqK1 = . (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 = . K by A2, A1;
A7: bseq (K + 1) is convergent by Th12;
hence dseqK1 is convergent by A3, A5; :: thesis: lim dseqK1 = . (K + 1)
thus lim dseqK1 = (lim dseqK) + (lim (bseq (K + 1))) by
.= () + (eseq . (K + 1)) by
.= . (K + 1) by SERIES_1:def 1 ; :: thesis: verum
end;
then A8: for n being Nat st S1[n] holds
S1[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 = . 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 = . 0 ) )
assume A9: for n being Nat holds dseq0 . n = (Partial_Sums (cseq n)) . 0 ; :: thesis: ( dseq0 is convergent & lim dseq0 = . 0 )
now :: thesis: for n being Element of NAT holds dseq0 . n = () . n
let n be Element of NAT ; :: thesis: dseq0 . n = () . n
thus dseq0 . n = (Partial_Sums (cseq n)) . 0 by A9
.= (cseq n) . 0 by SERIES_1:def 1
.= () . n by Th3 ; :: thesis: verum
end;
then A10: dseq0 = bseq 0 by FUNCT_2:63;
hence dseq0 is convergent by Th12; :: thesis: lim dseq0 = . 0
thus lim dseq0 = eseq . 0 by
.= . 0 by SERIES_1:def 1 ; :: thesis: verum
end;
then A11: S1[ 0 ] ;
thus for n being Nat holds S1[n] from NAT_1:sch 2(A11, A8); :: thesis: verum