:: deftheorem Def2 defines l_norm RSSPACE3:def 2 :
for b₁ being Function of the_set_of_l1RealSequences,REAL holds
( b₁ = l_norm iff for x being object st x in the_set_of_l1RealSequences holds
b₁ . x = Sum (abs (seq_id x)) );