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