let X be non empty set ; :: thesis: R_Normed_Algebra_of_BoundedFunctions X is RealLinearSpace
P1: for v being VECTOR of (R_Normed_Algebra_of_BoundedFunctions X) holds 1 * v = v by FUNCSDOM23;
R_Normed_Algebra_of_BoundedFunctions X is Algebra by LmAlgebra4;
hence R_Normed_Algebra_of_BoundedFunctions X is RealLinearSpace by LmAlgebra, P1; :: thesis: verum