let V be non empty right_complementable Abelian add-associative right_zeroed Algebra-like AlgebraStr ; :: thesis:
assume A1: V is scalar-mult-cancelable ; :: thesis:
B0: 1 * (0. V) = 0. V by RLVECT123;
A2: for v being VECTOR of V holds 1 * v = v

proof

let v be VECTOR of V; :: thesis:
B1: (1 * v) - (1 * v) = 0. V by RLVECT_1:28;
(1 * v) + (1 * (- v)) = 1 * (v + (- v)) by FUNCSDOM:def 20;
then (1 * v) + (1 * (- v)) = 1 * (0. V) by RLVECT_1:16;
then B2: - (1 * v) = 1 * (- v) by B0, B1, RLVECT_1:21;
1 * v = (1 * 1) * v
.= 1 * (1 * v) by FUNCSDOM:def 20 ;
then (1 * (1 * v)) - (1 * v) = 0. V by RLVECT_1:28;
then 1 * ((1 * v) - v) = 0. V by B2, FUNCSDOM:def 20;
then (1 * v) - v = 0. V by A1, DefSMC;
hence 1 * v = v by RLVECT_1:35; :: thesis:

end;

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

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

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

end;

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