let X be non empty compact TopSpace; :: thesis: for F being Point of (R_Normed_Algebra_of_ContinuousFunctions X) st F = 0. (R_Normed_Algebra_of_ContinuousFunctions X) holds
0 = ||.F.||
let F be Point of (R_Normed_Algebra_of_ContinuousFunctions X); :: thesis: ( F = 0. (R_Normed_Algebra_of_ContinuousFunctions X) implies 0 = ||.F.|| )
assume A1: F = 0. (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;
A2: ||.F.|| = ||.F1.|| by FUNCT_1:72;
F = X --> 0 by A1, ThB18;
then F1 = 0. (R_Normed_Algebra_of_BoundedFunctions the carrier of X) by C0SP1:26;
hence 0 = ||.F.|| by A2, C0SP1:29; :: thesis: verum