let X be non empty compact TopSpace; :: thesis: for F being Point of (R_Normed_Algebra_of_ContinuousFunctions X) holds 0 <= ||.F.||
let F be Point of (R_Normed_Algebra_of_ContinuousFunctions X); :: thesis: 0 <= ||.F.||
reconsider F1 = F as Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) by LMX01;
||.F.|| = ||.F1.|| by FUNCT_1:72;
hence 0 <= ||.F.|| by C0SP1:28; :: thesis: verum