defpred S₁[ object ] means (seq_id $1) rto_power p is summable ;
consider IT being set such that
A2: for x being object holds
( x in IT iff ( x in the_set_of_RealSequences & S₁[x] ) ) from XBOOLE_0:sch 1();
for x being object 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 absolutely_summable

proof

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

now :: thesis: for n being Nat holds rseq . n = 0

let n be Nat; :: thesis: rseq . n = 0
thus rseq . n = |.((seq_id Zeroseq) . n).| to_power p by Def1
.= 0 to_power p by ABSVALUE:2, RSSPACE:4
.= 0 by A1, POWER:def 2 ; :: thesis: verum

end;

hence (seq_id Zeroseq) rto_power p is absolutely_summable by COMSEQ_3:3; :: thesis: verum

end;

then not IT is empty by A2;
then reconsider IT = IT as non empty Subset of Linear_Space_of_RealSequences by A3;
take IT ; :: thesis: for x being set holds
( x in IT iff ( x in the_set_of_RealSequences & (seq_id x) rto_power p is summable ) )
thus for x being set holds
( x in IT iff ( x in the_set_of_RealSequences & (seq_id x) rto_power p is summable ) ) by A2; :: thesis: verum