seq_id Zeroseq is absolutely_summable

proof

reconsider rseq = seq_id Zeroseq as Real_Sequence ;
for n being Nat holds rseq . n = 0 ;
hence seq_id Zeroseq is absolutely_summable by COMSEQ_3:3; :: thesis: verum

end;

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