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