theorem Th3: :: PROB_3:3

for g being Real
for f being Real_Sequence st ex k being Nat st
for n being Nat st k <= n holds
f . n = g holds
( f is convergent & lim f = g )