let R be Ring; :: thesis: for G, H being LeftMod of R
for f being strict Morphism of G,H holds {f} is LModMorphism_DOMAIN of G,H
let G, H be LeftMod of R; :: thesis: for f being strict Morphism of G,H holds {f} is LModMorphism_DOMAIN of G,H
let f be strict Morphism of G,H; :: thesis: {f} is LModMorphism_DOMAIN of G,H
for x being Element of {f} holds x is strict Morphism of G,H by TARSKI:def 1;
hence {f} is LModMorphism_DOMAIN of G,H by Th2; :: thesis: verum