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

end;

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