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 Th22, Th23;
hence R_Normed_Algebra_of_BoundedFunctions X is RealLinearSpace by Lm2; :: thesis: verum