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