let R be Ring; :: thesis: for V being RightMod of R
for v being Vector of V
for W being Submodule of V holds v in v + W
let V be RightMod of R; :: 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 Th17, RLVECT_1:def 4;
hence v in v + W ; :: thesis: verum