theorem :: RFUNCT_2:7

for seq being Real_Sequence st seq is convergent & ( for n being Nat holds seq . n <= 0 ) holds
lim seq <= 0