∀ {A : Type u_1} {B : Type u_2} [inst : NonUnitalNonAssocSemiring A] [inst_1 : Star A]
  [inst_2 : NonUnitalNonAssocSemiring B] [inst_3 : Star B] (toNonUnitalRingHom : A →ₙ+* B)
  (map_star' : ∀ (a : A), toNonUnitalRingHom.toFun (star a) = star (toNonUnitalRingHom.toFun a))
  (toNonUnitalRingHom_1 : A →ₙ+* B)
  (map_star'_1 : ∀ (a : A), toNonUnitalRingHom_1.toFun (star a) = star (toNonUnitalRingHom_1.toFun a)),
  ({ toNonUnitalRingHom := toNonUnitalRingHom, map_star' := map_star' } =
      { toNonUnitalRingHom := toNonUnitalRingHom_1, map_star' := map_star'_1 }) =
    (toNonUnitalRingHom = toNonUnitalRingHom_1)