theorem Th46: :: C0SP3:46

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