∀ {α : Type u_7} {β : Type u_8} [inst : MulZeroOneClass α] [inst_1 : MulZeroOneClass β] [inst_2 : SizeOf α]
  [inst_3 : SizeOf β] (toZeroHom : ZeroHom α β) (map_one' : toZeroHom.toFun 1 = 1)
  (map_mul' : ∀ (x y : α), toZeroHom.toFun (x * y) = toZeroHom.toFun x * toZeroHom.toFun y),
  sizeOf { toZeroHom := toZeroHom, map_one' := map_one', map_mul' := map_mul' } = 1 + sizeOf toZeroHom + sizeOf map_one'