theorem :: REAL_NS3:20

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