for I being set
for G being TopGroup
for f being Function of ([#] (OrderedFIN I)), the carrier of G
for x being Point of G
for B being basis of (BOOL2F (NeighborhoodSystem x)) holds
( x in lim_f f iff for b being Element of B ex i being Element of (OrderedFIN I) st
for j being Element of (OrderedFIN I) st i <= j holds
f . j in b )