consider G being LeftMod of R;
take {(ID G)} ; :: thesis: for x being Element of {(ID G)} holds x is strict LModMorphism of R
let x be Element of {(ID G)}; :: thesis: x is strict LModMorphism of R
thus x is strict LModMorphism of R by TARSKI:def 1; :: thesis: verum