theorem Th20: :: SEQFUNC2:11

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
for f being PartFunc of D, the carrier of Y st H is_point_conv_on X holds
( f = lim (H,X) iff ( dom f = X & ( for x being Element of D st x in X holds
for p being Real st p > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
||.(((H . n) /. x) - (f /. x)).|| < p ) ) )