:: deftheorem Def13 defines lim SEQFUNC:def 13 :
for D being non empty set
for H being Functional_Sequence of D,REAL
for X being set st H is_point_conv_on X holds
for b₄ being PartFunc of D,REAL holds
( b₄ = lim (H,X) iff ( dom b₄ = X & ( for x being Element of D st x in dom b₄ holds
b₄ . x = lim (H # x) ) ) );