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