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 holds
( x in lim_f s iff for v being Subset of X st v in V /\ (NeighborhoodSystem (0. X)) holds
ex i being Nat st
for j being Nat st i <= j holds
s . j in x + v )