:: deftheorem Def1 defines max_norm REAL_NS3:def 1 :
for n being Nat st not n is empty holds
for b₂ being Function of (REAL n),REAL holds
( b₂ = max_norm n iff for x being Element of REAL n holds
( b₂ . x in rng (abs x) & ( for i being Nat st i in dom x holds
(abs x) . i <= b₂ . x ) ) );