∀ {R : Type u_5} {S : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : PartialOrder S] [inst_3 : SizeOf R]
  [inst_4 : SizeOf S] (toMulHom : R →ₙ* S) (nonneg' : ∀ (x : R), 0 ≤ toMulHom.toFun x)
  (eq_zero' : ∀ (x : R), toMulHom.toFun x = 0 ↔ x = 0)
  (add_le' : ∀ (x y : R), toMulHom.toFun (x + y) ≤ toMulHom.toFun x + toMulHom.toFun y),
  sizeOf { toMulHom := toMulHom, nonneg' := nonneg', eq_zero' := eq_zero', add_le' := add_le' } = 1 + sizeOf toMulHom