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