:: deftheorem defMophVW defines ZQMorph ZMODUL07:def 2 :
for R being Ring
for V being LeftMod of R
for W being Subspace of V
for b₄ being linear-transformation of V,(VectQuot (V,W)) holds
( b₄ = ZQMorph (V,W) iff for v being Element of V holds b₄ . v = v + W );