reconsider z = z as Element of COMPLEX by XCMPLX_0:def 2;
the Mult of V . [z,v] is Element of V ;
hence the Mult of V . [z,v] is Element of V ; :: thesis: verum