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