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