reconsider VW = the carrier of W as Subset of V by Def8;
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 Lm5; :: thesis: verum