theorem Th1: :: PROB_1:1

for r being Real
for seq being Real_Sequence st ex n being Nat st
for m being Nat st n <= m holds
seq . m = r holds
( seq is convergent & lim seq = r )