let V be Z_Module; :: thesis: for v being VECTOR of V
for W being Submodule of V holds v in v + W
let v be VECTOR of V; :: thesis: for W being Submodule of V holds v in v + W
let W be Submodule of V; :: thesis: v in v + W
( v + (0. V) = v & 0. V in W ) by Th33, RLVECT_1:4;
hence v in v + W ; :: thesis: verum