let R be Ring; :: thesis: for f being strict LModMorphism of R holds {f} is LModMorphism_DOMAIN of R
let f be strict LModMorphism of R; :: thesis: {f} is LModMorphism_DOMAIN of R
for x being Element of {f} holds x is strict LModMorphism of R by TARSKI:def 1;
hence {f} is LModMorphism_DOMAIN of R by Def2; :: thesis: verum