defpred S₁[ set ] means (seq_id $1) rto_power p is summable ;
consider IT being set such that
A2: for x being set holds
( x in IT iff ( x in the_set_of_RealSequences & S₁[x] ) ) from XBOOLE_0:sch 1();
for x being set st x in IT holds
x in the_set_of_RealSequences by A2;
then A3: IT is Subset of the_set_of_RealSequences by TARSKI:def 3;
(seq_id Zeroseq) rto_power p is summable

proof

reconsider rseq = (seq_id Zeroseq) rto_power p as Real_Sequence ;

now

let n be Element of NAT ; :: thesis: rseq . n = 0
thus rseq . n = (abs ((seq_id Zeroseq) . n)) to_power p by Def1
.= (abs 0) to_power p by RSSPACE:def 6
.= 0 to_power p by ABSVALUE:2
.= 0 by A1, POWER:def 2 ; :: thesis: verum

end;

hence (seq_id Zeroseq) rto_power p is summable by COMSEQ_3:3, SERIES_1:35; :: thesis: verum

end;

then not IT is empty by A2;
hence ex b₁ being non empty Subset of Linear_Space_of_RealSequences st
for x being set holds
( x in b₁ iff ( x in the_set_of_RealSequences & (seq_id x) rto_power p is summable ) ) by A2, A3, RSSPACE:def 7; :: thesis: verum