defpred S_{1}[ object ] means seq_id $1 is bounded ;

consider IT being set such that

A1: for x being object holds

( x in IT iff ( x in the_set_of_ComplexSequences & S_{1}[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_{1} being Subset of Linear_Space_of_ComplexSequences st

for x being object holds

( x in b_{1} iff ( x in the_set_of_ComplexSequences & seq_id x is bounded ) )
by A1; :: thesis: verum

consider IT being set such that

A1: for x being object holds

( x in IT iff ( x in the_set_of_ComplexSequences & S

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

for x being object holds

( x in b