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