:: deftheorem Def2 defines sum_norm REAL_NS3:def 2 :
for n being Nat st not n is empty holds
for b₂ being Function of (REAL n),REAL holds
( b₂ = sum_norm n iff for x being Element of REAL n holds b₂ . x = Sum (abs x) );