let X be non empty set ; :: thesis: R_Normed_Algebra_of_BoundedFunctions X is RealLinearSpace
( ( for v being VECTOR of (R_Normed_Algebra_of_BoundedFunctions X) holds 1 * v = v ) & R_Normed_Algebra_of_BoundedFunctions X is Algebra ) by Th23, Th24;
hence R_Normed_Algebra_of_BoundedFunctions X is RealLinearSpace by Lm3; :: thesis: verum