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