theorem Th46: :: CC0SP2:46

for a being Complex
for X being non empty TopSpace
for F, G being Point of (C_Normed_Space_of_C_0_Functions X) holds
( ( ||.F.|| = 0 implies F = 0. (C_Normed_Space_of_C_0_Functions X) ) & ( F = 0. (C_Normed_Space_of_C_0_Functions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = |.a.| * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )