theorem :: CSSPACE4:1

for seq being Complex_Sequence holds
( ( seq is bounded & upper_bound (rng |.seq.|) = 0 ) iff for n being Nat holds seq . n = 0c ) by Lm7, Lm10;