:: deftheorem Def9 defines the_set_of_l2ComplexSequences CSSPACE:def 11 :
for b₁ being Subset of Linear_Space_of_ComplexSequences holds
( b₁ = the_set_of_l2ComplexSequences iff for x being object holds
( x in b₁ iff ( x in the_set_of_ComplexSequences & |.(seq_id x).| (#) |.(seq_id x).| is summable ) ) );