:: deftheorem Def6 defines lim COMSEQ_2:def 6 :
for s being Complex_Sequence st s is convergent holds
for b₂ being Complex holds
( b₂ = lim s iff for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((s . m) - b₂).| < p );