defpred S₁[ set ] means |.(seq_id $1).| (#) |.(seq_id $1).| is summable ;
consider IT being set such that
A1: for x being set holds
( x in IT iff ( x in the_set_of_ComplexSequences & S₁[x] ) ) from XBOOLE_0:sch 1();
for x being set st x in IT holds
x in the_set_of_ComplexSequences by A1;
then A2: IT is Subset of the_set_of_ComplexSequences by TARSKI:def 3;
|.(seq_id CZeroseq).| (#) |.(seq_id CZeroseq).| is absolutely_summable

proof

reconsider rseq = |.(seq_id CZeroseq).| (#) |.(seq_id CZeroseq).| as Real_Sequence ;

now :: thesis: for n being Element of NAT holds rseq . n = 0

let n be Element of NAT ; :: thesis: rseq . n = 0
thus rseq . n = (|.(seq_id CZeroseq).| . n) * (|.(seq_id CZeroseq).| . n) by SEQ_1:8
.= (|.(seq_id CZeroseq).| . n) * |.((seq_id CZeroseq) . n).| by VALUED_1:18
.= (|.(seq_id CZeroseq).| . n) * 0 by Def6, COMPLEX1:44
.= 0 ; :: thesis: verum

end;

hence |.(seq_id CZeroseq).| (#) |.(seq_id CZeroseq).| is absolutely_summable by COMSEQ_3:3; :: thesis: verum

end;

then not IT is empty by A1;
hence ex b₁ being Subset of Linear_Space_of_ComplexSequences st
( not b₁ is empty & ( for x being set holds
( x in b₁ iff ( x in the_set_of_ComplexSequences & |.(seq_id x).| (#) |.(seq_id x).| is summable ) ) ) ) by A1, A2; :: thesis: verum