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 Def7; :: thesis: verum