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