theorem Th18: :: C0SP2:18

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