theorem :: REAL_NS3:19

for X being finite-dimensional RealLinearSpace
for b being OrdBasis of RLSp2RVSp X
for x, y being Element of X
for a being Real st dim X <> 0 holds
( 0 <= (sum_norm (X,b)) . x & ( (sum_norm (X,b)) . x = 0 implies x = 0. X ) & ( x = 0. X implies (sum_norm (X,b)) . x = 0 ) & (sum_norm (X,b)) . (a * x) = |.a.| * ((sum_norm (X,b)) . x) & (sum_norm (X,b)) . (x + y) <= ((sum_norm (X,b)) . x) + ((sum_norm (X,b)) . y) )