let X be non empty compact TopSpace; :: thesis: for F being Point of (R_Normed_Algebra_of_ContinuousFunctions X) holds (Mult_ (ContinuousFunctions X),(RAlgebra the carrier of X)) . 1,F = F
let F be Point of (R_Normed_Algebra_of_ContinuousFunctions X); :: thesis: (Mult_ (ContinuousFunctions X),(RAlgebra the carrier of X)) . 1,F = F
set X1 = ContinuousFunctions X;
reconsider f1 = F as Element of ContinuousFunctions X ;
A1: [1,f1] in [:REAL ,(ContinuousFunctions X):] by ZFMISC_1:106;
thus (Mult_ (ContinuousFunctions X),(RAlgebra the carrier of X)) . 1,F = (the Mult of (RAlgebra the carrier of X) | [:REAL ,(ContinuousFunctions X):]) . 1,f1 by C0SP1:def 11
.= the Mult of (RAlgebra the carrier of X) . 1,f1 by A1, FUNCT_1:72
.= F by FUNCSDOM:23 ; :: thesis: verum