let V be non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative AlgebraStr ; :: thesis: ( V is scalar-mult-cancelable implies V is RealLinearSpace )
assume A1: V is scalar-mult-cancelable ; :: thesis: V is RealLinearSpace
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 RLVECT_1:def 5;
then ( (1 * v) - (1 * v) = 0. V & (1 * v) + (1 * (- v)) = 1 * (0. V) ) by RLVECT_1:5;
then A2: - (jj * v) = jj * (- v) by Th4, RLVECT_1:8;
1 * v = (1 * 1) * v
.= 1 * (1 * v) by RLVECT_1:def 7 ;
then (1 * (1 * v)) - (1 * v) = 0. V by RLVECT_1:15;
then 1 * ((1 * v) - v) = 0. V by A2, RLVECT_1:def 5;
then (jj * v) - v = 0. V by A1;
hence 1 * v = v by RLVECT_1:21; :: thesis: verum

end;

hence V is RealLinearSpace by RLVECT_1:def 8; :: thesis: verum