let X be non empty set ; :: thesis: RAlgebra X is RealLinearSpace
for v being VECTOR of (RAlgebra X) holds 1 * v = v by FUNCSDOM:12;
hence RAlgebra X is RealLinearSpace by Lm2; :: thesis: verum