theorem Th30: :: IRRAT_1:30

( dseq is convergent & lim dseq = Sum eseq )