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