theorem :: CARDFIL3:24

for N being RealNormSpace
for s being sequence of the carrier of (TopSpaceMetr (MetricSpaceNorm N))
for j being Nat holds s . j is Element of the carrier of (TopSpaceMetr (MetricSpaceNorm N)) ;