:: deftheorem defMophVW defines ZQMorph ZMODUL07:def 2 :
for V being Z_Module
for W being Submodule of V
for b₃ being linear-transformation of V,(Z_ModuleQuot (V,W)) holds
( b₃ = ZQMorph (V,W) iff for v being Element of V holds b₃ . v = v + W );