set z = ZERO (G,H);
( fun (ZERO (G,H)) is additive & fun (ZERO (G,H)) is homogeneous ) ;
hence ZERO (G,H) is LModMorphism-like by Def10; :: thesis: verum