take ZeroMap (G,H) ; :: thesis: for x, y being Element of G holds (ZeroMap (G,H)) . (x + y) = ((ZeroMap (G,H)) . x) + ((ZeroMap (G,H)) . y)
thus for x, y being Element of G holds (ZeroMap (G,H)) . (x + y) = ((ZeroMap (G,H)) . x) + ((ZeroMap (G,H)) . y) by Lm13; :: thesis: verum