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

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