defpred S1[ 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 & S1[x] ) ) from 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 = 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 = |.( . n).| to_power p by Def1
.= 0 to_power p by
.= 0 by ; :: 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 & () rto_power p is summable ) )

thus for x being set holds
( x in IT iff ( x in the_set_of_RealSequences & () rto_power p is summable ) ) by A2; :: thesis: verum