the carrier of W = (0. V) + W by VECTSP_4:60;
then the carrier of W is Coset of W by VECTSP_4:def 6;
then the carrier of W in CosetSet V,W ;
hence the carrier of W is Element of CosetSet V,W ; :: thesis: verum