:: deftheorem defines + RMOD_2:def 5 :
for R being Ring
for V being RightMod of R
for v being Vector of V
for W being Submodule of V holds v + W = { (v + u) where u is Vector of V : u in W } ;