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
A: 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;

B: 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;

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;

hence V is RealLinearSpace by A1, RLVECT_1:def 9, A, B; :: thesis: verum