for n being non empty Nat
for x being Element of REAL n holds
( (sum_norm n) . x <= n * ((max_norm n) . x) & (max_norm n) . x <= |.x.| & |.x.| <= (sum_norm n) . x )