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