∀ {R : Type u_2} {M : Type u_5} {N : Type u_6} [inst : Semiring R] [inst_1 : Monoid M] [inst_2 : Monoid N] (e : M ≃* N)
  (x : MonoidAlgebra R M) (n : N), ((MonoidAlgebra.mapDomainRingEquiv R e) x) n = x (e.symm n)