:: deftheorem Def1 defines -convergent CFDIFF_1:def 1 :
for x being Real
for IT being Complex_Sequence holds
( IT is x -convergent iff ( IT is convergent & lim IT = x ) );