set z = ZERO (G,H);
fun (ZERO (G,H)) is additive ;
hence ZERO (G,H) is GroupMorphism-like by Def18; :: thesis: verum