reconsider a = a as Real by XREAL_0:def 1;
the Mult of V . (a,v) is Element of V ;
hence the Mult of V . (a,v) is Element of V ; :: thesis: verum