:: deftheorem Def14 defines Lin RMOD_4:def 14 :
for R being domRing
for V being RightMod of R
for A being Subset of V
for b₄ being strict Submodule of V holds
( b₄ = Lin A iff the carrier of b₄ = { (Sum l) where l is Linear_Combination of A : verum } );