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