:: deftheorem Def10 defines Z_ModuleQuot ZMODUL02:def 10 :
for V being Z_Module
for W being Submodule of V
for b₃ being strict Z_Module holds
( b₃ = Z_ModuleQuot (V,W) iff ( the carrier of b₃ = CosetSet (V,W) & the addF of b₃ = addCoset (V,W) & 0. b₃ = zeroCoset (V,W) & the lmult of b₃ = lmultCoset (V,W) ) );