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();
A2: not IT is empty

proof

|.(seq_id CZeroseq ).| (#) |.(seq_id CZeroseq ).| is summable

proof

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

now

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

end;

then rseq is absolutely_summable by COMSEQ_3:3;
hence |.(seq_id CZeroseq ).| (#) |.(seq_id CZeroseq ).| is summable by SERIES_1:40; :: thesis: verum

end;

hence not IT is empty by A1; :: thesis: verum

end;

IT is Subset of the_set_of_ComplexSequences

proof

for x being set st x in IT holds
x in the_set_of_ComplexSequences by A1;
hence IT is Subset of the_set_of_ComplexSequences by TARSKI:def 3; :: thesis: verum

end;

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