let V be non empty right_complementable Abelian add-associative right_zeroed Algebra-like AlgebraStr ; :: thesis: ( ( for v being VECTOR of V holds 1 * v = v ) implies V is RealLinearSpace )
assume A1: for v being VECTOR of V holds 1 * v = v ; :: thesis: V is RealLinearSpace

A2: now

let a be real number ; :: thesis: for v, w being VECTOR of V holds a * (v + w) = (a * v) + (a * w)
a is Real by XREAL_0:def 1;
hence for v, w being VECTOR of V holds a * (v + w) = (a * v) + (a * w) by FUNCSDOM:def 20; :: thesis: verum

end;

A3: now

let a, b be real number ; :: thesis: for v being VECTOR of V holds (a + b) * v = (a * v) + (b * v)
( a is Real & b is Real ) by XREAL_0:def 1;
hence for v being VECTOR of V holds (a + b) * v = (a * v) + (b * v) by FUNCSDOM:def 20; :: thesis: verum

end;

now

let a, b be real number ; :: thesis: for v being VECTOR of V holds (a * b) * v = a * (b * v)
( a is Real & b is Real ) by XREAL_0:def 1;
hence for v being VECTOR of V holds (a * b) * v = a * (b * v) by FUNCSDOM:def 20; :: thesis: verum

end;

hence V is RealLinearSpace by A1, A2, A3, RLVECT_1:def 9; :: thesis: verum