reconsider D = {(ZERO (G,H))} as LModMorphism_DOMAIN of R by Th1;
take D ; :: thesis: for x being Element of D holds x is strict Morphism of G,H
thus for x being Element of D holds x is strict Morphism of G,H by TARSKI:def 1; :: thesis: verum