:: deftheorem Def21 defines LMULT LMOD_7:def 21 :
for K being Ring
for V being LeftMod of K
for W being Subspace of V
for b₄ being Function of [: the carrier of K, the carrier of (V . W):], the carrier of (V . W) holds
( b₄ = LMULT W iff for r being Scalar of K
for S being Element of (V . W) holds b₄ . (r,S) = r * S );