theorem Th3: :: COMSEQ_3:3

for rseq being Real_Sequence st ( for n being Nat holds rseq . n = 0 ) holds
rseq is absolutely_summable