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