theorem Th9: :: IRRAT_1:9

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