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