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