0. V = a * (0. V) by VECTSP_1:14;
then 0. V in a * V ;
hence 0. V is Element of a * V ; :: thesis: verum