for R being domRing
for V being RightMod of R
for A being Subset of V
for W being strict Submodule of V st 0. R <> 1_ R & A = the carrier of W holds
Lin A = W