seq_id CZeroseq is bounded

proof

reconsider seq = seq_id CZeroseq as Complex_Sequence ;
for n being Nat holds |.(seq . n).| < jj by COMPLEX1:44;
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