set G = the LeftMod of R;
set z = ZERO ( the LeftMod of R, the LeftMod of R);
ZERO ( the LeftMod of R, the LeftMod of R) is LModMorphism-like ;
hence ex b₁ being LModMorphismStr over R st
( b₁ is strict & b₁ is LModMorphism-like ) ; :: thesis: verum