for x, y being Element of G holds (ZeroMap G,H) . (x + y) = ((ZeroMap G,H) . x) + ((ZeroMap G,H) . y) by Lm13;
hence ZeroMap G,H is Homomorphism of G,H by Def19; :: thesis: verum