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 Lm1;
||.F.|| = ||.F1.|| by FUNCT_1:49;
hence 0 <= ||.F.|| by C0SP1:27; :: thesis: verum