for N being RealNormSpace
for s being sequence of the carrier of (TopSpaceMetr (MetricSpaceNorm N))
for x being Point of (TopSpaceMetr (MetricSpaceNorm N)) holds
( x in lim_f s iff for n being positive Nat ex i being Nat st
for j being Nat st i <= j holds
||.((# x) - (# (s . j))).|| < 1 / n )