for K being Ring
for V being LeftMod of K
for a being Vector of V
for W being Subspace of V holds a .. W is Element of (V . W) ;