let X be non empty set ; :: thesis: for F being Point of (R_Normed_Algebra_of_BoundedFunctions X) holds (Mult_ (BoundedFunctions X),(RAlgebra X)) . 1,F = F
let F be Point of (R_Normed_Algebra_of_BoundedFunctions X); :: thesis: (Mult_ (BoundedFunctions X),(RAlgebra X)) . 1,F = F
set X1 = BoundedFunctions X;
reconsider f1 = F as Element of BoundedFunctions X ;
A1: [1,f1] in [:REAL ,(BoundedFunctions X):] by ZFMISC_1:106;
thus (Mult_ (BoundedFunctions X),(RAlgebra X)) . 1,F = (the Mult of (RAlgebra X) | [:REAL ,(BoundedFunctions X):]) . 1,f1 by Def11
.= the Mult of (RAlgebra X) . 1,f1 by A1, FUNCT_1:72
.= F by FUNCSDOM:23 ; :: thesis: verum