reconsider a = a as Element of INT by INT_1:def 2;
the Mult of V . (a,v) is Element of V ;
hence the Mult of V . (a,v) is Element of V ; :: thesis: verum