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 )
A1: for a being real number
for v, w being VECTOR of V holds a * (v + w) = (a * v) + (a * w)

proof

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

end;

A2: for a, b being real number
for v being VECTOR of V holds (a + b) * v = (a * v) + (b * v)

proof

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

end;

A3: for a, b being real number
for v being VECTOR of V holds (a * b) * v = a * (b * v)

proof

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

end;

assume for v being VECTOR of V holds 1 * v = v ; :: thesis: V is RealLinearSpace
hence V is RealLinearSpace by A1, A2, A3, RLVECT_1:def 9; :: thesis: verum