∀ {R : Type u} {A : Type v} {inst : CommSemiring R} {inst_1 : StarRing R} {inst_2 : Semiring A} {inst_3 : StarRing A}
  {inst_4 : Algebra R A} {inst_5 : StarModule R A} {toSubalgebra : Subalgebra R A}
  {star_mem' : ∀ {a : A}, a ∈ toSubalgebra.carrier → star a ∈ toSubalgebra.carrier} {toSubalgebra_1 : Subalgebra R A}
  {star_mem'_1 : ∀ {a : A}, a ∈ toSubalgebra_1.carrier → star a ∈ toSubalgebra_1.carrier},
  { toSubalgebra := toSubalgebra, star_mem' := star_mem' } =
      { toSubalgebra := toSubalgebra_1, star_mem' := star_mem'_1 } →
    toSubalgebra = toSubalgebra_1