:: deftheorem Def2 defines the_set_of_RealSequences_l^ LP_SPACE:def 2 :
for p being Real st p >= 1 holds
for b₂ being non empty Subset of Linear_Space_of_RealSequences holds
( b₂ = the_set_of_RealSequences_l^ p iff for x being set holds
( x in b₂ iff ( x in the_set_of_RealSequences & (seq_id x) rto_power p is summable ) ) );