reconsider VW = the carrier of W as Subset of V by Def2;
take VW ; :: thesis: ex v being VECTOR of V st VW = v + W
take 0. V ; :: thesis: VW = (0. V) + W
thus VW = (0. V) + W by Lm2; :: thesis: verum