let D be non empty set ; :: thesis: for R being Ring
for G, H being LeftMod of R holds
( D is LModMorphism_DOMAIN of G,H iff for x being Element of D holds x is strict Morphism of G,H )
let R be Ring; :: thesis: for G, H being LeftMod of R holds
( D is LModMorphism_DOMAIN of G,H iff for x being Element of D holds x is strict Morphism of G,H )
let G, H be LeftMod of R; :: thesis: ( D is LModMorphism_DOMAIN of G,H iff for x being Element of D holds x is strict Morphism of G,H )
thus ( D is LModMorphism_DOMAIN of G,H implies for x being Element of D holds x is strict Morphism of G,H ) by Def3; :: thesis: ( ( for x being Element of D holds x is strict Morphism of G,H ) implies D is LModMorphism_DOMAIN of G,H )
thus ( ( for x being Element of D holds x is strict Morphism of G,H ) implies D is LModMorphism_DOMAIN of G,H ) :: thesis: verum

proof

assume A1: for x being Element of D holds x is strict Morphism of G,H ; :: thesis: D is LModMorphism_DOMAIN of G,H
then for x being Element of D holds x is strict LModMorphism of R ;
then reconsider D9 = D as LModMorphism_DOMAIN of R by Def2;
for x being Element of D9 holds x is strict Morphism of G,H by A1;
hence D is LModMorphism_DOMAIN of G,H by Def3; :: thesis: verum

end;