let X be non empty set ; :: thesis: for F being Point of (C_Normed_Algebra_of_BoundedFunctions X) holds (Mult_ ((ComplexBoundedFunctions X),(CAlgebra X))) . (1r,F) = F
let F be Point of (C_Normed_Algebra_of_BoundedFunctions X); :: thesis: (Mult_ ((ComplexBoundedFunctions X),(CAlgebra X))) . (1r,F) = F
set X1 = ComplexBoundedFunctions X;
reconsider f1 = F as Element of ComplexBoundedFunctions X ;
A1: [1r,f1] in [:COMPLEX,(ComplexBoundedFunctions X):] ;
(Mult_ ((ComplexBoundedFunctions X),(CAlgebra X))) . (1r,F) = ( the Mult of (CAlgebra X) | [:COMPLEX,(ComplexBoundedFunctions X):]) . (1r,f1) by Def3
.= the Mult of (CAlgebra X) . (1r,f1) by A1, FUNCT_1:49
.= F by CFUNCDOM:12 ;
hence (Mult_ ((ComplexBoundedFunctions X),(CAlgebra X))) . (1r,F) = F ; :: thesis: verum