defpred S_{1}[ 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_{1}[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

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

consider IT being set such that

A2: 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 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

then
not IT is empty
by A2;
reconsider rseq = (seq_id Zeroseq) rto_power p as Real_Sequence ;

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

hence
(seq_id Zeroseq) rto_power p is absolutely_summable
by COMSEQ_3:3; :: thesis: verumlet 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;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

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