theorem :: SEQ_4:30

for seq being Real_Sequence st ( for n being Nat holds seq . n = 1 / (n + 1) ) holds
( seq is convergent & lim seq = 0 ) by Th28, Th29;