|.(seq_id CZeroseq).| (#) |.(seq_id CZeroseq).| is absolutely_summable by Lm1;
hence not the_set_of_l2ComplexSequences is empty by Def9; :: thesis: verum