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: [jj,f1] in [:REAL,(ContinuousFunctions X):] ;
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:49
.= F by FUNCSDOM:12 ; :: thesis: verum