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

now

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 1 * v = 1 * v1 by Th8;
hence 1 * v = v by FUNCSDOM:12; :: thesis: verum

end;

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