:: deftheorem Def20 defines * LMOD_7:def 20 :
for K being Ring
for V being LeftMod of K
for W being Subspace of V
for r being Scalar of K
for S, b₆ being Element of (V . W) holds
( b₆ = r * S iff for a being Vector of V st S = a . W holds
b₆ = (r * a) . W );