take ZeroMap (G,H) ; :: thesis: ZeroMap (G,H) is additive
thus ZeroMap (G,H) is additive ; :: thesis: verum