for X being LinearTopSpace
for s being sequence of the carrier of X
for x being Point of X
for V being local_base of X
for B being Subset-Family of X st B = { (x + U) where U is Subset of X : ( U in V & U is a_neighborhood of 0. X ) } holds
( x in lim_f s iff for v being Element of B ex i being Nat st
for j being Nat st i <= j holds
s . j in v )