let X be non empty compact TopSpace; :: thesis: for F being Point of (C_Normed_Algebra_of_ContinuousFunctions X) holds (Mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))) . (1r,F) = F
let F be Point of (C_Normed_Algebra_of_ContinuousFunctions X); :: thesis: (Mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))) . (1r,F) = F
set X1 = CContinuousFunctions X;
reconsider f1 = F as Element of CContinuousFunctions X ;
A1: [1,f1] in [:COMPLEX,(CContinuousFunctions X):] by ZFMISC_1:87;
(Mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))) . (1,F) = ( the Mult of (CAlgebra the carrier of X) | [:COMPLEX,(CContinuousFunctions X):]) . (1,f1) by CC0SP1:def 3
.= the Mult of (CAlgebra the carrier of X) . (1,f1) by A1, FUNCT_1:49
.= F by CFUNCDOM:12 ;
hence (Mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))) . (1r,F) = F ; :: thesis: verum