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