:: deftheorem Def8 defines the_set_of_l2RealSequences RSSPACE:def 11 :
for b₁ being Subset of Linear_Space_of_RealSequences holds
( b₁ = the_set_of_l2RealSequences iff for x being object holds
( x in b₁ iff ( x in the_set_of_RealSequences & (seq_id x) (#) (seq_id x) is summable ) ) );