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