let X be non empty compact TopSpace; 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); (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
; verum