:: deftheorem Def2 defines cl_norm CSSPACE3:def 2 :
for b₁ being Function of the_set_of_l1ComplexSequences,REAL holds
( b₁ = cl_norm iff for x being object st x in the_set_of_l1ComplexSequences holds
b₁ . x = Sum |.(seq_id x).| );