:: deftheorem Def12 defines .. LMOD_7:def 12 :
for K being Ring
for V being LeftMod of K
for W being Subspace of V
for b₄ being set holds
( b₄ = V .. W iff for x being set holds
( x in b₄ iff ex a being Vector of V st x = a + W ) );