let X be non empty compact TopSpace; :: thesis: for F being Point of (C_Normed_Algebra_of_ContinuousFunctions X) st ||.F.|| = 0 holds
F = 0. (C_Normed_Algebra_of_ContinuousFunctions X)
let F be Point of (C_Normed_Algebra_of_ContinuousFunctions X); :: thesis: ( ||.F.|| = 0 implies F = 0. (C_Normed_Algebra_of_ContinuousFunctions X) )
reconsider F1 = F as Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) by Lm1;
( ||.F1.|| = 0 iff F1 = 0. (C_Normed_Algebra_of_BoundedFunctions the carrier of X) ) by CC0SP1:25;
hence ( ||.F.|| = 0 implies F = 0. (C_Normed_Algebra_of_ContinuousFunctions X) ) by Lm7, FUNCT_1:49; :: thesis: verum