let V be non empty right_complementable add-associative right_zeroed Algebra-like 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 FUNCSDOM:def 20;
then (a * (0. V)) + (a * (0. V)) = a * (0. V) by RLVECT_1:10;
then (a * (0. V)) + (a * (0. V)) = (a * (0. V)) + (0. V) by RLVECT_1:10;
hence a * (0. V) = 0. V by RLVECT_1:21; :: thesis: verum