let X be non empty set ; :: thesis: R_Algebra_of_BoundedFunctions X is RealLinearSpace

now :: thesis: for v being VECTOR of (R_Algebra_of_BoundedFunctions X) holds 1 * v = v

let v be VECTOR of (R_Algebra_of_BoundedFunctions X); :: thesis: 1 * v = v
reconsider v1 = v as VECTOR of (RAlgebra X) by TARSKI:def 3;
R_Algebra_of_BoundedFunctions X is Subalgebra of RAlgebra X by Th6;
then jj * v = jj * v1 by Th8;
hence 1 * v = v by FUNCSDOM:12; :: thesis: verum

end;

hence R_Algebra_of_BoundedFunctions X is RealLinearSpace by Lm2; :: thesis: verum