:: deftheorem Def10 defines lim MESFUN7C:def 10 :
for X being non empty set
for f being Functional_Sequence of X,COMPLEX
for b₃ being PartFunc of X,COMPLEX holds
( b₃ = lim f iff ( dom b₃ = dom (f . 0) & ( for x being Element of X st x in dom b₃ holds
b₃ . x = lim (f # x) ) ) );