the carrier of W = (0. V) + W by VECTSP_4:45;
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