theorem :: SEQ_4:15

for seq being Real_Sequence st abs seq is convergent & lim (abs seq) = 0 holds
( seq is convergent & lim seq = 0 )