defpred S_{1}[ 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_RealSequences & S_{1}[x] ) )
from XBOOLE_0:sch 1();

for x being object st x in IT holds

x in the_set_of_RealSequences by A1;

then IT is Subset of the_set_of_RealSequences by TARSKI:def 3;

hence ex b_{1} being Subset of Linear_Space_of_RealSequences st

for x being object holds

( x in b_{1} iff ( x in the_set_of_RealSequences & (seq_id x) (#) (seq_id x) is summable ) )
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_RealSequences & S

for x being object st x in IT holds

x in the_set_of_RealSequences by A1;

then IT is Subset of the_set_of_RealSequences by TARSKI:def 3;

hence ex b

for x being object holds

( x in b