:: deftheorem Def8 defines Morphism MOD_2:def 8 :
for R being Ring
for G, H being LeftMod of R
for b₄ being LModMorphism of R holds
( b₄ is Morphism of G,H iff ( dom b₄ = G & cod b₄ = H ) );