for R being Ring
for f being strict LModMorphism of R holds {f} is LModMorphism_DOMAIN of R