:: deftheorem Def3 defines LModMorphism_DOMAIN MODCAT_1:def 3 :
for R being Ring
for G, H being LeftMod of R
for b₄ being LModMorphism_DOMAIN of R holds
( b₄ is LModMorphism_DOMAIN of G,H iff for x being Element of b₄ holds x is strict Morphism of G,H );