theorem Th9: :: COMSEQ_2:9

for s being Complex_Sequence st ex g being Complex st
for n being Nat holds s . n = g holds
s is convergent