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