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