:: deftheorem defines / LMOD_7:def 22 :
for K being Ring
for V being LeftMod of K
for W being Subspace of V holds V / W = ModuleStr(# the carrier of (V . W), the addF of (V . W),((0. V) . W),(LMULT W) #);