let V be non empty right_complementable Abelian add-associative right_zeroed Algebra-like AlgebraStr ; :: thesis: ( ( for v being VECTOR of V holds 1 * v = v ) implies V is RealLinearSpace )
assume A1: for v being VECTOR of V holds 1 * v = v ; :: thesis: V is RealLinearSpace
( ( 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 A1, RLVECT_1:def 9; :: thesis: verum