theorem :: CARDFIL3:15

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 b being Element of Balls x ex i being Nat st
for j being Nat st i <= j holds
s . j in b ) by Th6;