seq_id CZeroseq is absolutely_summable

proof

reconsider cseq = seq_id CZeroseq as Complex_Sequence ;
for n being Nat holds cseq . n = 0c by CSSPACE:4;
hence seq_id CZeroseq is absolutely_summable by COMSEQ_3:51; :: thesis: verum

end;

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