set vq = v + (p (*) V);
v + (p (*) V) is Coset of p (*) V by VECTSP_4:def 6;
then v + (p (*) V) in { A where A is Coset of p (*) V : verum } ;
then v + (p (*) V) is Element of CosetSet (V,(p (*) V)) ;
hence v + (p (*) V) is Vector of (Z_MQ_VectSp (V,p)) by VECTSP10:def 6; :: thesis: verum