for n being non empty Nat
for x, y being Element of REAL n
for a being Real holds
( 0 <= (sum_norm n) . x & ( (sum_norm n) . x = 0 implies x = 0* n ) & ( x = 0* n implies (sum_norm n) . x = 0 ) & (sum_norm n) . (a * x) = |.a.| * ((sum_norm n) . x) & (sum_norm n) . (x + y) <= ((sum_norm n) . x) + ((sum_norm n) . y) )