let X be non empty compact TopSpace; :: thesis: ||.(0. (C_Normed_Algebra_of_ContinuousFunctions X)).|| = 0
set F = 0. (C_Normed_Algebra_of_ContinuousFunctions X);
reconsider F1 = 0. (C_Normed_Algebra_of_ContinuousFunctions X) 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 ||.(0. (C_Normed_Algebra_of_ContinuousFunctions X)).|| = 0 by Lm7, FUNCT_1:49; :: thesis: verum