for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative AlgebraStr st V is scalar-mult-cancelable holds
V is RealLinearSpace