theorem CLTh37: :: NORMSP_3:69

for X being RealNormSpace
for Y being Subset of X
for f, g being Point of (ClNLin Y)
for a being Real holds
( ( ||.f.|| = 0 implies f = 0. (ClNLin Y) ) & ( f = 0. (ClNLin Y) implies ||.f.|| = 0 ) & ||.(a * f).|| = |.a.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )