for K being Nat
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 )