for S being RealNormSpace
for seq being sequence of S
for x being set holds
( x in rng seq iff ex n being Nat st x = seq . n )