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