theorem :: LMOD_7:18

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 Vector of (V / W) ;