seq_id Zeroseq is absolutely_summable

proof

reconsider rseq = seq_id Zeroseq as Real_Sequence ;
for n being Element of NAT holds rseq . n = 0 by RSSPACE:def 6;
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