defpred S_{1}[ 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 );

_{1}[n] holds

S_{1}[n + 1]
;

_{1}[ 0 ]
;

thus for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A11, A8); :: thesis: verum

( 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) )

then A8:
for n being Nat st S( 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_{1}( Nat) -> set = (Partial_Sums (cseq $1)) . K;

consider dseqK being Real_Sequence such that

A1: for n being Nat holds dseqK . n = H_{1}(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) )

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;( 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

consider dseqK being Real_Sequence such that

A1: for n being Nat holds dseqK . n = H

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

then A5:
dseqK1 = dseqK + (bseq (K + 1))
by FUNCT_2:63;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;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

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

S

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 )

then A11:
S( 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 )

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;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

then A10:
dseq0 = bseq 0
by FUNCT_2:63;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;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

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

thus for n being Nat holds S