:: deftheorem Def13 defines lim SEQFUNC2:def 9 :
for D being non empty set
for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y
for X being set st H is_point_conv_on X holds
for b₅ being PartFunc of D, the carrier of Y 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) ) ) );