seq_id CZeroseq is bounded

proof

reconsider seq = seq_id CZeroseq as Complex_Sequence ;
for n being Element of NAT holds |.(seq . n).| < 1 by COMPLEX1:44, CSSPACE:def 6;
hence seq_id CZeroseq is bounded by COMSEQ_2:8; :: thesis: verum

end;

hence not the_set_of_BoundedComplexSequences is empty by Def1; :: thesis: verum