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 )
assume A1: V is scalar-mult-cancelable ; :: thesis: V is RealLinearSpace
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: 1 * v = v
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: verum

end;

( ( for a being Real
for v, w being VECTOR of V holds a * (v + w) = (a * v) + (a * w) ) & ( for a, b being Real
for v being VECTOR of V holds (a + b) * v = (a * v) + (b * v) ) & ( for a, b being Real
for v being VECTOR of V holds (a * b) * v = a * (b * v) ) ) by FUNCSDOM:def 20;
hence V is RealLinearSpace by A2, RLVECT_1:def 9; :: thesis: verum