theorem Th7: :: NCFCONT1:7

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