theorem Th22: :: CSSPACE4:22

for X being non empty set
for Y being ComplexNormSpace
for f, g being Point of (C_NormSpace_of_BoundedFunctions (X,Y))
for c being Complex holds
( ( ||.f.|| = 0 implies f = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) ) & ( f = 0. (C_NormSpace_of_BoundedFunctions (X,Y)) implies ||.f.|| = 0 ) & ||.(c * f).|| = |.c.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )