theorem Th19: :: REAL_NS3:18

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 <= (max_norm (X,b)) . x & ( (max_norm (X,b)) . x = 0 implies x = 0. X ) & ( x = 0. X implies (max_norm (X,b)) . x = 0 ) & (max_norm (X,b)) . (a * x) = |.a.| * ((max_norm (X,b)) . x) & (max_norm (X,b)) . (x + y) <= ((max_norm (X,b)) . x) + ((max_norm (X,b)) . y) )