let V be non empty right_complementable Abelian add-associative right_zeroed Algebra-like AlgebraStr ; :: thesis: ( V is scalar-mult-cancelable implies V is RealLinearSpace )
A1: 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;

A2: 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 A3: V is scalar-mult-cancelable ; :: thesis: V is RealLinearSpace
A4: for v being VECTOR of V holds 1 * v = v

proof

let v be VECTOR of V; :: thesis: 1 * v = v
(1 * v) + (1 * (- v)) = 1 * (v + (- v)) by FUNCSDOM:def 20;
then ( (1 * v) - (1 * v) = 0. V & (1 * v) + (1 * (- v)) = 1 * (0. V) ) by RLVECT_1:16, RLVECT_1:28;
then A5: - (1 * v) = 1 * (- v) by Th4, 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 A5, FUNCSDOM:def 20;
then (1 * v) - v = 0. V by A3, Def12;
hence 1 * v = v by RLVECT_1:35; :: thesis: verum

end;

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;

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