let V be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative AlgebraStr ; :: thesis: for a being Real holds a * (0. V) = 0. V
let a be Real; :: thesis: a * (0. V) = 0. V
(a * (0. V)) + (a * (0. V)) = a * ((0. V) + (0. V)) by RLVECT_1:def 5;
then (a * (0. V)) + (a * (0. V)) = a * (0. V) ;
then (a * (0. V)) + (a * (0. V)) = (a * (0. V)) + (0. V) ;
hence a * (0. V) = 0. V by RLVECT_1:8; :: thesis: verum